HomeTheorem List (p. 3 of 10)
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List
| Home |
brismu
bridi Theorem List (p. 3 of 10) |
< Previous Next >
|
|
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List | ||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Axiom | ax-qi1 201 | 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 202 | Inference form of ax-qi1 201 (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 203 | Inference form of ax-qi1 201. 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 | ||
| Axiom | ax-qi2 204 | A variant of ax-qi1 201 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 205 | Inference form of ax-qi2 204 (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 206 | Inference form of ax-qi2 204. 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 207 | {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 208 | {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 209 | 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 210 | 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 211 | 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 212* | 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 213* | 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 | ||
| Syntax | sbdu 214 | Identity as a binary relation. |
| selbri du | ||
| Definition | df-du 215 | 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 216 | Inference form of df-du 215 (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 217 | Sugared inference form of df-du 215 (Contributed by la korvo, 23-Jun-2024.) |
| ⊢ ko'a du ko'e ⊢ go
ko'a bu'a
gi ko'e bu'a | ||
| Theorem | duri 218 | Reverse inference form of df-du 215 (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 219 | Sugared reverse inference form of df-du 215 (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 220 | {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 221 | {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 222 | 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 223 | {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 224 | An internal version of du-symi 223 (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ ganai ko'a du ko'e gi ko'e du ko'a | ||
| Theorem | du-sym-go 225 | An internal version of du-symi 223 (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ go ko'a du ko'e gi ko'e du ko'a | ||
| Theorem | se-du-elim 226 | {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 227* | 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 228* | First-order quantifier substitution. |
| ⊢ ganai ro da zo'u da du de gi ro de zo'u de du da | ||
| Axiom | ax-ro-int 229* | 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 230 |
|
| bridi cei'i | ||
| Definition | df-ceihi 231 | 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 232 or ceihi-nf 404. |
| ⊢ go cei'i gi ko'a du ko'a | ||
| Theorem | ceihi 232 | {cei'i} is always true. (Contributed by la korvo, 18-Jul-2023.) |
| ⊢ cei'i | ||
| Theorem | mp-ceihi 233 | A proposition implied by {cei'i} is always true. (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ ganai cei'i gi broda ⊢ broda | ||
| Theorem | k-ceihi 234 | {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 235 |
|
| bridi gai'o | ||
| Syntax | bnk 236 | Syntax for negation over an empty row of quantifiers. |
| bridi naku broda | ||
| Definition | df-naku 237 | Traditional definition of intuitionistic negation. |
| ⊢ go naku broda gi ganai broda gi gai'o | ||
| Theorem | naku-uncur 238 | Uncurried form of df-naku 237 (Contributed by la korvo, 20-Aug-2023.) |
| ⊢ ganai ge naku broda gi broda gi gai'o | ||
| Theorem | lnc 239 | 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 240 | 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 241 | Inference form of df-naku 237 (Contributed by la korvo, 9-Aug-2023.) |
| ⊢ naku broda ⊢ ganai
broda gi gai'o | ||
| Theorem | nakuii 242 | Inference form of df-naku 237 (Contributed by la korvo, 9-Aug-2023.) |
| ⊢ naku broda ⊢ broda ⊢ gai'o | ||
| Theorem | nakuri 243 | Reverse inference form of df-naku 237 (Contributed by la korvo, 9-Aug-2023.) |
| ⊢ ganai broda gi gai'o ⊢ naku
broda | ||
| Theorem | na-gaiho 244 | {gai'o} is uninhabited. (Contributed by la korvo, 9-Aug-2023.) |
| ⊢ naku gai'o | ||
| Axiom | ax-sdo 245 | 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 246 | Inference form of ax-sdo 245 (Contributed by la korvo, 9-Aug-2023.) |
| ⊢ ganai broda gi naku broda ⊢ naku
broda | ||
| Theorem | sdod 247 | Deduction form of ax-sdo 245 (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ ganai broda gi ganai brode gi naku brode ⊢ ganai
broda gi naku brode | ||
| Axiom | ax-efq 248 | 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 249 | Inference form of ax-efq 248 (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ naku broda ⊢ ganai
broda gi brode | ||
| Theorem | efqd 250 | Deduction form of ax-efq 248 (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ ganai broda gi naku brode ⊢ ganai
broda gi ganai brode gi brodi | ||
| Theorem | efqii 251 | Inference form of ax-efq 248 (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ naku broda ⊢ broda ⊢ brode | ||
| Theorem | con2d 252 | 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 253 | 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 254 | 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 255 | The standard contrapositive inference. (Contributed by la korvo, 1-Jan-2025.) |
| ⊢ ganai broda gi naku brode ⊢ ganai
brode gi naku broda | ||
| Theorem | nakunaku 256 | Double negation is a functor. (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ ganai broda gi naku naku broda | ||
| Theorem | nakunakui 257 | Inference form of nakunaku 256 (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ broda ⊢ naku
naku broda | ||
| Theorem | nsyl 258 | 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 259 | 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 260 |
|
| bridi gonai broda gi brode | ||
| Definition | df-gonai 261 | 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 262 | Inference form of df-gonai 261 (Contributed by la korvo, 8-Aug-2023.) |
| ⊢ gonai broda gi brode ⊢ ge
ga broda gi brode gi naku
ge broda gi brode | ||
| Theorem | gonaiil 263 | Inference form of df-gonai 261 (Contributed by la korvo, 8-Aug-2023.) |
| ⊢ gonai broda gi brode ⊢ ga
broda gi brode | ||
| Theorem | gonaiir 264 | Inference form of df-gonai 261 (Contributed by la korvo, 8-Aug-2023.) |
| ⊢ gonai broda gi brode ⊢ naku
ge broda gi brode | ||
| Theorem | gonairi 265 | Reverse inference form of df-gonai 261 (Contributed by la korvo, 8-Aug-2023.) |
| ⊢ ge
ga broda gi brode gi naku
ge broda gi brode ⊢ gonai
broda gi brode | ||
| Syntax | sjonai 266 |
|
| sumti ko'a .onai ko'e | ||
| Definition | df-onai 267 | Definition of {.onai} in terms of {gonai}. By analogy with forethought version of example 12.2-5 from [CLL] p. 14. |
| ⊢ go ko'a .onai ko'e bo'a gi gonai ko'a bo'a gi ko'e bo'a | ||
| Theorem | onaii 268 | Inference form of df-onai 267 (Contributed by la korvo, 16-Aug-2023.) |
| ⊢ ko'a .onai ko'e
bo'a ⊢
gonai ko'a bo'a gi ko'e
bo'a | ||
| Theorem | onairi 269 | Reverse inference form of df-onai 267 (Contributed by la korvo, 16-Aug-2023.) |
| ⊢ gonai ko'a bo'a gi
ko'e bo'a ⊢ ko'a .onai ko'e
bo'a | ||
| Syntax | sbjonai 270* |
|
| selbri bu'a jonai bu'e | ||
| Definition | df-jonai 271* | Definition of {jonai} in terms of {gonai}. By analogy with example 12.2-5 of [CLL] p. 14. |
| ⊢ go ko'a bu'a jonai bu'e ko'e gi gonai ko'a bu'a ko'e gi ko'a bu'e ko'e | ||
| Theorem | jonaii 272* | Inference form of df-jonai 271 (Contributed by la korvo, 16-Aug-2023.) |
| ⊢ ko'a bu'a
jonai bu'e ko'e ⊢ gonai
ko'a bu'a ko'e gi ko'a
bu'e ko'e | ||
| Theorem | jonairi 273* | Reverse inference form of df-jonai 271 (Contributed by la korvo, 16-Aug-2023.) |
| ⊢ gonai ko'a bu'a ko'e gi ko'a
bu'e ko'e ⊢ ko'a bu'a
jonai bu'e ko'e | ||
| Syntax | tgihonai 274 |
|
| brirebla bo'a gi'onai bo'e | ||
| Definition | df-gihonai 275 | Definition of {gi'onai} in terms of {gonai}. |
| ⊢ go ko'a bo'a gi'onai bo'e gi gonai ko'a bo'a gi ko'a bo'e | ||
| Theorem | gihonaii 276 | Inference form of df-gihonai 275 (Contributed by la korvo, 14-Aug-2023.) |
| ⊢ ko'a bo'a
gi'onai bo'e ⊢ gonai
ko'a bo'a
gi ko'a bo'e | ||
| Theorem | gihonairi 277 | Inference form of df-gihonai 275 (Contributed by la korvo, 14-Aug-2023.) |
| ⊢ gonai ko'a bo'a gi
ko'a bo'e ⊢ ko'a bo'a
gi'onai bo'e | ||
| Syntax | bgagin 278 |
|
| bridi ga broda ginai brode | ||
| Syntax | bgogin 279 |
|
| bridi go broda ginai brode | ||
| Definition | df-ginai-ga 280 |
|
| ⊢ go ga brode ginai broda gi ganai broda gi brode | ||
| Definition | df-ginai-go 281 |
|
| ⊢ go go broda ginai brode gi gonai broda gi brode | ||
We build the various non-logical connectives, which express combinations of elements of relations beyond truth tables. In particular, we develop the notion of set membership. | ||
| Syntax | sbcmima 282 |
|
| selbri cmima | ||
| Syntax | sbselcmi 283 |
|
| selbri selcmi | ||
| Definition | df-selcmi 284 |
|
| ⊢ go ko'a selcmi ko'e gi ko'a se cmima ko'e | ||
| Axiom | ax-cmima-ext 285 | The Axiom of Extensionality: If no elements differ in elementhood for two sets, then they are the same set. |
| ⊢ ganai ro da zo'u da cmima ko'a .o ko'e gi ko'a du ko'e | ||
| Syntax | snomei 286 |
|
| sumti le nomei ku | ||
| Definition | df-nomei 287 | {le nomei} is the empty set. Literally it is the set with zero cardinality. By standard folklore of sets, it is unique up to isomorphism, justifying {le}. |
| ⊢ naku ko'a cmima le nomei ku | ||
| Theorem | nomei-gaiho 288 | If the empty set is inhabited, then there is a contradiction. (Contributed by la korvo, 16-May-2024.) |
| ⊢ ko'a cmima le nomei
ku ⊢ gai'o | ||
| Syntax | sbpamei 289 |
|
| selbri pamei | ||
| Definition | df-pamei 290 | The singleton set is the unique set whose elements are all isomorphic. Since we use the full semantics of second-order logic, we cannot construct the witness isomorphisms. As a compromise, we construct the isomorphism between any two elements of any particular singleton set. |
| ⊢ go ko'a pamei ko'e .e ko'i gi ko'e du ko'i | ||
| Theorem | pameii 291 | Inference form of df-pamei 290 (Contributed by la korvo, 16-May-2024.) |
| ⊢ ko'a pamei ko'e .e ko'i ⊢ ko'e du ko'i | ||
| Theorem | pameiii 292 | Inference form of df-pamei 290 (Contributed by la korvo, 16-May-2024.) |
| ⊢ ko'a pamei ko'e ⊢ ko'a pamei ko'i ⊢ ko'e du ko'i | ||
| Axiom | ax-pamei-cmima 293 | The singleton set has one element. |
| ⊢ ganai ko'a pamei ko'e gi ko'e cmima ko'a | ||
| Syntax | sbgripau 294 |
|
| selbri gripau | ||
| Definition | df-gripau 295 | Definition of {gripau} in terms of {cmima} and {na.a}. Defined in section 7 of [CLL] p. 18 based on the gloss "set-part". This definition is phrased with an implicit universal quantification instead of {ro da zo'u da cmima ko'a na.a ko'e} or {ro da poi ke'a cmima ko'a ku'o zo'u da cmima ko'e} for succinctness and ease of theorem-proving. |
| ⊢ go ko'a gripau ko'e gi ko'i cmima ko'a na.a ko'e | ||
| Theorem | gripaui 296 | Inference form of df-gripau 295 (Contributed by la korvo, 15-Jul-2024.) |
| ⊢ ko'a gripau ko'e ⊢ ko'i cmima ko'a na.a ko'e | ||
| Theorem | gripauri 297 | Reverse inference form of df-gripau 295 (Contributed by la korvo, 15-Jul-2024.) |
| ⊢ ko'i cmima ko'a na.a ko'e ⊢ ko'a gripau ko'e | ||
| Theorem | gripauis 298 | Inference form of df-gripau 295 (Contributed by la korvo, 19-Jul-2024.) |
| ⊢ ko'a gripau ko'e ⊢ ganai
ko'i cmima ko'a gi ko'i
cmima ko'e | ||
| Theorem | gripauiis 299 | Inference form of df-gripau 295 (Contributed by la korvo, 15-Jul-2024.) |
| ⊢ ko'a gripau ko'e ⊢ ko'i cmima ko'a ⊢ ko'i cmima ko'e | ||
| Theorem | gripauris 300 | Reverse inference form of df-gripau 295 (Contributed by la korvo, 19-Jul-2024.) |
| ⊢ ganai ko'i cmima ko'a gi ko'i
cmima ko'e ⊢ ko'a gripau ko'e | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |