HomeTheorem List (p. 3 of 11)
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List
| Home |
brismu
bridi Theorem List (p. 3 of 11) |
< Previous Next >
|
|
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List | ||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | o-com 201 | {.o} commutes. (Contributed by la korvo, 14-Aug-2023.) |
| ⊢ go ko'a .o ko'e bo'a gi ko'e .o ko'a bo'a | ||
| Theorem | o-comi 202 | Inference form of o-com 201 (Contributed by la korvo, 16-Jul-2023.) |
⊢ ko'a .o ko'e
bo'a  ⊢ ko'e .o ko'a
bo'a | ||
| Theorem | o-refl 203 | {.o} is reflexive over any brirebla. (Contributed by la korvo, 14-Aug-2024.) |
| ⊢ ko'a .o ko'a bo'a | ||
| Syntax | sbjo 204* |
|
| selbri bu'a jo bu'e | ||
| Definition | df-jo 205* | Definition of {jo} in terms of {go}. By analogy with example 12.2-5 of [CLL] p. 14. |
| ⊢ go ko'a bu'a jo bu'e ko'e gi go ko'a bu'a ko'e gi ko'a bu'e ko'e | ||
| Theorem | joi 206* | Inference form of df-jo 205 (Contributed by la korvo, 17-Jul-2023.) |
| ⊢ ko'a bu'a jo
bu'e ko'e ⊢ go
ko'a bu'a ko'e gi ko'a
bu'e ko'e | ||
| Theorem | jori 207* | Reverse inference form of df-jo 205 (Contributed by la korvo, 17-Jul-2023.) |
| ⊢ go ko'a bu'a ko'e gi ko'a
bu'e ko'e ⊢ ko'a bu'a jo
bu'e ko'e | ||
| Syntax | tgiho 208 |
|
| brirebla bo'a gi'o bo'e | ||
| Definition | df-giho 209 | Definition of {gi'o} in terms of {go}. |
| ⊢ go ko'a bo'a gi'o bo'e gi go ko'a bo'a gi ko'a bo'e | ||
| Theorem | gihoi 210 | Inference form of df-giho 209 (Contributed by la korvo, 14-Aug-2023.) |
| ⊢ ko'a bo'a
gi'o bo'e ⊢ go ko'a bo'a gi
ko'a bo'e | ||
| Theorem | gihori 211 | Inference form of df-giho 209 (Contributed by la korvo, 14-Aug-2023.) |
| ⊢ go ko'a bo'a gi
ko'a bo'e ⊢ ko'a bo'a
gi'o bo'e | ||
| Syntax | sbs 212 | If {bu'a} is a selbri, then so is {se bu'a}. |
| selbri se bu'a | ||
| Definition | df-se 213 | Definition of {se} as a swap of terbri. Implied by example 11.1-2 of [CLL] p. 5. |
| ⊢ go ko'e se bu'a ko'a gi ko'a bu'a ko'e | ||
| Theorem | sei 214 | From example 11.1-2 of [CLL] p. 5, where {mipramido} and {do se pramimi} are equivalent. Inference form of df-se 213 (Contributed by la korvo, 17-Jul-2023.) |
| ⊢ ko'e se bu'a
ko'a ⊢ ko'a bu'a ko'e | ||
| Theorem | seri 215 | From example 11.1-2 of [CLL] p. 5, where {mipramido} and {do se pramimi} are equivalent. Reverse inference form of df-se 213 (Contributed by la korvo, 17-Jul-2023.) |
| ⊢ ko'a bu'a ko'e ⊢ ko'e se bu'a
ko'a | ||
| Theorem | se-invo 216 | {se} is an involution. (Contributed by la korvo, 18-Jul-2023.) |
| ⊢ ko'a se se bu'a ko'e ⊢ ko'a bu'a ko'e | ||
| Theorem | se-dual 217* | Self-duality property for {se}. (Contributed by la korvo, 30-Jun-2024.) |
| ⊢ ko'a bu'a naja
bu'e ko'e ⊢ ko'e se bu'a
naja se bu'e ko'a | ||
| Theorem | se-dual-l 218* | Shift {se} to the left of an implication. (Contributed by la korvo, 30-Jun-2024.) |
| ⊢ ko'a bu'a naja
se bu'e ko'e ⊢ ko'e se bu'a
naja bu'e ko'a | ||
| Theorem | se-dual-r 219* | Shift {se} to the right of an implication. (Contributed by la korvo, 30-Jun-2024.) |
| ⊢ ko'a se bu'a
naja bu'e ko'e ⊢ ko'e bu'a naja
se bu'e ko'a | ||
| Theorem | se-ganaii 220* | Convert selbri on both sides of an implication simultaneously. (Contributed by la korvo, 19-Jul-2024.) |
| ⊢ ganai ko'a bu'a ko'e gi ko'i
bu'e ko'o ⊢ ganai
ko'e se bu'a ko'a gi
ko'o se bu'e ko'i | ||
| Theorem | se-ganair 221* | Convert selbri on both sides of an implication simultaneously. (Contributed by la korvo, 19-Jul-2024.) |
| ⊢ ganai ko'a se bu'a
ko'e gi ko'i se bu'e
ko'o ⊢ ganai
ko'e bu'a ko'a gi ko'o
bu'e ko'i | ||
| Syntax | brd 222 | Syntax for first-order universal quantification. |
| bridi ro da zo'u broda | ||
| Syntax | brb 223 | Syntax for second-order universal quantification. |
| bridi ro bu'a zo'u broda | ||
| Axiom | ax-gen1 224 | Axiom of first-order generalization. |
| ⊢ broda ⊢ ro
da zo'u broda | ||
| Theorem | mpg1 225 | Modus ponens with generalization. (Contributed by la korvo, 3-Jan-2025.) |
⊢ ganai
ro da zo'u broda gi brode  ⊢ broda ⊢ brode | ||
| Theorem | big1 226 | Modus ponens with generalization. (Contributed by la korvo, 9-Jul-2025.) |
| ⊢ go
ro da zo'u broda gi brode ⊢ broda ⊢ brode | ||
| Axiom | ax-gen2 227 | Axiom of second-order generalization. |
| ⊢ broda ⊢ ro
bu'a zo'u broda | ||
| Axiom | ax-spec1 228 | Axiom of first-order specialization. |
| ⊢ ganai ro da zo'u broda gi broda | ||
| Theorem | spec1i 229 | Inference form of ax-spec1 228 (Contributed by la korvo, 22-Jun-2024.) |
| ⊢ ro da zo'u broda ⊢ broda | ||
| Theorem | spec1d 230 | Deduction form of ax-spec1 228 (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ ganai broda gi ro da zo'u brode ⊢ ganai
broda gi brode | ||
| Theorem | spec1s 231 | Generalize an antecedent. (Contributed by la korvo, 8-Jul-2025.) |
| ⊢ ganai broda gi brode ⊢ ganai
ro da zo'u broda gi brode | ||
| Axiom | ax-spec2 232 | Axiom of second-order specialization, by analogy with ax-spec1 228 |
| ⊢ ganai ro bu'a zo'u broda gi broda | ||
| Theorem | spec2i 233 | Inference form of ax-spec2 232 (Contributed by la korvo, 23-Jun-2024.) |
| ⊢ ro bu'a zo'u broda ⊢ broda | ||
| Axiom | ax-qi1 234 | Axiom of quantified implication: if {ganai broda gi brode} under some universal quantifier, then the universal quantification of {broda} implies the universal quantification of {brode}. Relationally, the tuples of the consequent might not have the same data as the tuples of the antecedent; we only know that they exist, not that they are related. |
| ⊢ ganai ro da zo'u ganai broda gi brode gi ganai ro da zo'u broda gi ro da zo'u brode | ||
| Theorem | qi1i 235 | Inference form of ax-qi1 234 (Contributed by la korvo, 23-Jun-2024.) |
| ⊢ ro da zo'u ganai broda gi brode ⊢ ganai
ro da zo'u broda gi ro da zo'u brode | ||
| Theorem | qi1-mp 236 | Inference form of ax-qi1 234. Like ax-mp 10 under {ro da}. (Contributed by la korvo, 23-Jun-2024.) |
| ⊢ ro da zo'u ganai broda gi brode ⊢ ro
da zo'u broda ⊢ ro
da zo'u brode | ||
| Theorem | qi1q 237 | Quantify over both sides of an implication. (Contributed by la korvo, 8-Jul-2025.) |
| ⊢ ganai broda gi brode ⊢ ganai
ro da zo'u broda gi ro da zo'u brode | ||
| Theorem | alrimih 238 | An inference. (Contributed by la korvo, 9-Jul-2025.) |
| ⊢ ganai broda gi ro da zo'u broda ⊢ ganai
broda gi brode ⊢ ganai
broda gi ro da zo'u brode | ||
| Axiom | ax-qi2 239 | A variant of ax-qi1 234 for second-order quantifiers. Very few claims will be invariant under free choice of {bu'a}, but those that are should be subject to this transformation by analogy to first-order reasoning and an appeal to set theory. |
| ⊢ ganai ro bu'a zo'u ganai broda gi brode gi ganai ro bu'a zo'u broda gi ro bu'a zo'u brode | ||
| Theorem | qi2i 240 | Inference form of ax-qi2 239 (Contributed by la korvo, 23-Jun-2024.) |
| ⊢ ro bu'a zo'u ganai broda gi brode ⊢ ganai
ro bu'a zo'u broda gi ro bu'a zo'u brode | ||
| Theorem | qi2-mp 241 | Inference form of ax-qi2 239. Like ax-mp 10 under {ro bu'a}. (Contributed by la korvo, 23-Jun-2024.) |
| ⊢ ro bu'a zo'u ganai broda gi brode ⊢ ro
bu'a zo'u broda ⊢ ro
bu'a zo'u brode | ||
| Axiom | ax-ro-inst-2u 242 | {ro bu'a} may be instantiated with any selbri. As example 13.3 of [CLL] p. 16 notes, this will be of limited use, and is included largely to allow for a second-order definition of equality. |
| brirebla bo'a ⊢ ro
bu'e zo'u ko'a bu'e ⊢ ko'a bo'a | ||
| Axiom | ax-ro-inst-1u 243 | {ro da} may be instantiated with any sumti. |
| sumti ko'a ⊢ ro
da zo'u da bo'a ⊢ ko'a bo'a | ||
| Theorem | ro2-mp 244 | Modus ponens under {ro bu'a}. (Contributed by la korvo, 23-Jun-2024.) |
| ⊢ ro bu'a zo'u broda ⊢ ganai
broda gi brode ⊢ ro
bu'a zo'u brode | ||
| Theorem | ro2-bi 245 | Biconditional modus ponens under {ro bu'a}. (Contributed by la korvo, 16-Jul-2023.) |
| ⊢ ro bu'a zo'u broda ⊢ go
broda gi brode ⊢ ro
bu'a zo'u brode | ||
| Theorem | ro2-bi-rev 246 | Biconditional modus ponens under {ro bu'a}. (Contributed by la korvo, 16-Aug-2023.) |
| ⊢ ro bu'a zo'u broda ⊢ go
brode gi broda ⊢ ro
bu'a zo'u brode | ||
| Axiom | ax-ro1-com 247* | First-order universal quantifiers commute. |
| ⊢ ganai ro da zo'u ro de zo'u broda gi ro de zo'u ro da zo'u broda | ||
| Theorem | ro1-coms 248* | Swap quantifiers on the antecedent. (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ ganai
ro da zo'u
ro de zo'u broda gi brode ⊢ ganai
ro de zo'u
ro da zo'u broda gi brode | ||
| Axiom | ax-ro1-nf 249 | First-order universal quantifiers bind their variables. |
| ⊢ ganai ro da zo'u broda gi ro da zo'u ro da zo'u broda | ||
| Syntax | sbdu 250 | Identity as a binary relation. |
| selbri du | ||
| Definition | df-du 251 | A second-order characterization of identity which is non-first-order-izable. |
| ⊢ go ko'a du ko'e gi ro bu'a zo'u ko'a .o ko'e bu'a | ||
| Theorem | dui 252 | Inference form of df-du 251 (Contributed by la korvo, 18-Jul-2023.) |
| ⊢ ko'a du ko'e ⊢ ro
bu'a zo'u ko'a .o ko'e
bu'a | ||
| Theorem | duis 253 | Sugared inference form of df-du 251 (Contributed by la korvo, 23-Jun-2024.) |
| ⊢ ko'a du ko'e ⊢ go
ko'a bu'a
gi ko'e bu'a | ||
| Theorem | duri 254 | Reverse inference form of df-du 251 (Contributed by la korvo, 18-Jul-2023.) |
| ⊢ ro bu'a zo'u ko'a
.o ko'e bu'a ⊢ ko'a du ko'e | ||
| Theorem | duris 255 | Sugared reverse inference form of df-du 251 (Contributed by la korvo, 23-Jun-2024.) |
| ⊢ go ko'a bu'a gi
ko'e bu'a ⊢ ko'a du ko'e | ||
| Theorem | du-refl 256 | {du} is reflexive. (Contributed by la korvo, 16-Aug-2023.) (Shortened by la korvo, 23-Jun-2024.) |
| ⊢ ko'a du ko'a | ||
| Theorem | du-trans 257 | {du} is transitive. (Contributed by la korvo, 16-Aug-2023.) (Shortened by la korvo, 23-Jun-2024.) |
| ⊢ ko'a du ko'e ⊢ ko'e du ko'i ⊢ ko'a du ko'i | ||
| Axiom | ax-du-trans 258 | A not-quite-transitive law of equality. |
| ⊢ ganai ko'a du ko'e gi ganai ko'a du ko'i gi ko'e du ko'i | ||
| Theorem | du-symi 259 | {du} is symmetric. (Contributed by la korvo, 16-Aug-2023.) (Shortened by la korvo, 23-Jun-2024.) |
| ⊢ ko'a du ko'e ⊢ ko'e du ko'a | ||
| Theorem | du-sym-ganai 260 | An internal version of du-symi 259 (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ ganai ko'a du ko'e gi ko'e du ko'a | ||
| Theorem | du-sym-go 261 | An internal version of du-symi 259 (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ go ko'a du ko'e gi ko'e du ko'a | ||
| Theorem | se-du-elim 262 | {se du} may be replaced with {du}. Theorem Cat.Allegory.Base.dual-id in [1Lab] p. 0. (Contributed by la korvo, 9-Jul-2023.) |
| ⊢ ko'a se du
ko'e ⊢ ko'a du ko'e | ||
| Axiom | ax-vsub 263* | An axiom of variable substitution. |
| ⊢ ganai da du de gi ganai ro de zo'u broda gi ro da zo'u ganai da du de gi broda | ||
| Axiom | ax-ro1-sub 264* | First-order quantifier substitution. |
| ⊢ ganai ro da zo'u da du de gi ro de zo'u de du da | ||
| Axiom | ax-ro-int 265* | First-order universal quantifier introduction with a scope gadget. |
| ⊢ ga ro di zo'u di du da gi ga ro di zo'u di du de gi ro di zo'u ganai da du de gi ro di zo'u da du de | ||
| Syntax | bceihi 266 |
|
| bridi cei'i | ||
| Definition | df-ceihi 267 | The predicate which is always true. Note that both sides are relational: the left-hand side definitionally only has one inhabitant, so this definition asserts that {ko'a du ko'a} is only true via one path. For related statements which reinforce this idea, see ceihi 268 or ceihi-nf 443. |
| ⊢ go cei'i gi ko'a du ko'a | ||
| Theorem | ceihi 268 | {cei'i} is always true. (Contributed by la korvo, 18-Jul-2023.) |
| ⊢ cei'i | ||
| Theorem | mp-ceihi 269 | A proposition implied by {cei'i} is always true. (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ ganai cei'i gi broda ⊢ broda | ||
| Theorem | ceihi-term 270 | {cei'i} is the terminal object. (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ ganai broda gi cei'i | ||
Lojban classically contains a {na} which may slide around in a prenex and between connectives. To be constructive, we will more carefully introduce {naku} negation within the prenex first, and then justify various simplifications and rearrangements. | ||
| Syntax | bgaiho 271 |
|
| bridi gai'o | ||
| Syntax | bnk 272 | Syntax for negation over an empty row of quantifiers. |
| bridi naku broda | ||
| Definition | df-naku 273 | Traditional definition of intuitionistic negation. |
| ⊢ go naku broda gi ganai broda gi gai'o | ||
| Theorem | naku-uncur 274 | Uncurried form of df-naku 273 (Contributed by la korvo, 20-Aug-2023.) |
| ⊢ ganai ge naku broda gi broda gi gai'o | ||
| Theorem | lnc 275 | The law of non-contradiction. No bridi is simultaneously inhabited and uninhabited. (Contributed by la korvo, 19-Sep-2024.) |
| ⊢ naku ge naku broda gi broda | ||
| Theorem | lnci 276 | The law of non-contradiction. If a bridi is simultaneously inhabited and uninhabited, then we reach an absurdity. (Contributed by la korvo, 20-Aug-2023.) |
| ⊢ ge broda gi naku broda ⊢ gai'o | ||
| Theorem | nakui 277 | Inference form of df-naku 273 (Contributed by la korvo, 9-Aug-2023.) |
| ⊢ naku broda ⊢ ganai
broda gi gai'o | ||
| Theorem | nakuii 278 | Inference form of df-naku 273 (Contributed by la korvo, 9-Aug-2023.) |
| ⊢ naku broda ⊢ broda ⊢ gai'o | ||
| Theorem | nakuri 279 | Reverse inference form of df-naku 273 (Contributed by la korvo, 9-Aug-2023.) |
| ⊢ ganai broda gi gai'o ⊢ naku
broda | ||
| Theorem | na-gaiho 280 | {gai'o} is uninhabited. (Contributed by la korvo, 9-Aug-2023.) |
| ⊢ naku gai'o | ||
| Axiom | ax-sdo 281 | The principle of self-defeating objects. If an object's existence would imply that it doesn't exist -- usually via contradiction -- then it doesn't exist. As a special case, if some tuple's membership in a relation would imply non-membership in that relation, then it's not a member. For a survey of this principle across maths, see [Tao]. |
| ⊢ ganai ganai broda gi naku broda gi naku broda | ||
| Theorem | sdoi 282 | Inference form of ax-sdo 281 (Contributed by la korvo, 9-Aug-2023.) |
| ⊢ ganai broda gi naku broda ⊢ naku
broda | ||
| Theorem | sdod 283 | Deduction form of ax-sdo 281 (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ ganai broda gi ganai brode gi naku brode ⊢ ganai
broda gi naku brode | ||
| Axiom | ax-efq 284 | The principle of explosion. If a tuple both is and is not a member of some relation, then we are inconsistent and any theorem whatsoever may be derived. The short name "efq" comes from the Latin phrase, "ex falso quodlibet". |
| ⊢ ganai naku broda gi ganai broda gi brode | ||
| Theorem | efqi 285 | Inference form of ax-efq 284 (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ naku broda ⊢ ganai
broda gi brode | ||
| Theorem | efqd 286 | Deduction form of ax-efq 284 (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ ganai broda gi naku brode ⊢ ganai
broda gi ganai brode gi brodi | ||
| Theorem | efqii 287 | Inference form of ax-efq 284 (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ naku broda ⊢ broda ⊢ brode | ||
| Theorem | gaiho-init 288 | From falsity, anything is possible. (Contributed by la korvo, 14-Jul-2025.) |
| ⊢ ganai gai'o gi broda | ||
| Theorem | con2d 289 | A contrapositive deduction. (Contributed by la korvo, 1-Jan-2025.) |
| ⊢ ganai broda gi ganai brode gi naku brodi ⊢ ganai
broda gi ganai brodi gi naku brode | ||
| Theorem | mt2d 290 | Deduction form of modus tollens. (Contributed by la korvo, 1-Jan-2025.) |
| ⊢ ganai broda gi brode ⊢ ganai
broda gi ganai brodi gi naku brode ⊢ ganai
broda gi naku brodi | ||
| Theorem | nsyl3 291 | A negated syllogism. Can be seen as a deduction form of modus tollens. (Contributed by la korvo, 1-Jan-2025.) |
| ⊢ ganai broda gi naku brode ⊢ ganai
brodi gi brode ⊢ ganai
brodi gi naku broda | ||
| Theorem | con2i 292 | The standard contrapositive inference. (Contributed by la korvo, 1-Jan-2025.) |
| ⊢ ganai broda gi naku brode ⊢ ganai
brode gi naku broda | ||
| Theorem | nakunaku 293 | Double negation is a functor. (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ ganai broda gi naku naku broda | ||
| Theorem | nakunakui 294 | Inference form of nakunaku 293 (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ broda ⊢ naku
naku broda | ||
| Theorem | nsyl 295 | A negated syllogism. Can be seen as a deduction form of modus tollens. (Contributed by la korvo, 1-Jan-2025.) |
| ⊢ ganai broda gi naku brode ⊢ ganai
brodi gi brode ⊢ ganai
broda gi naku brodi | ||
| Theorem | stewart 296 | A syllogism underlying the Swallowing Elephants puzzle from chapter 4 of [Stewart] p. 22. (Contributed by la korvo, 1-Jan-2025.) |
| ⊢ ganai broda gi brode ⊢ ganai
brodi gi brodo ⊢ ganai
brodu gi brodi ⊢ ganai
brode gi naku brodo ⊢ ganai
broda gi naku brodu | ||
The final of our five essential connectives. As with disjunctions, we can introduce all versions of mutual exclusion at once. | ||
| Syntax | bgon 297 |
|
| bridi gonai broda gi brode | ||
| Definition | df-gonai 298 | Standard constructive definition of mutual exclusion ("the exclusive OR"), based on the mnemonic given to computer scientists in the USA and UK: "It's cake or tea, but not cake and tea." |
| ⊢ go gonai broda gi brode gi ge ga broda gi brode gi naku ge broda gi brode | ||
| Theorem | gonaii 299 | Inference form of df-gonai 298 (Contributed by la korvo, 8-Aug-2023.) |
| ⊢ gonai broda gi brode ⊢ ge
ga broda gi brode gi naku
ge broda gi brode | ||
| Theorem | gonaiil 300 | Inference form of df-gonai 298 (Contributed by la korvo, 8-Aug-2023.) |
| ⊢ gonai broda gi brode ⊢ ga
broda gi brode | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |