![]() |
brismu
bridi Theorem List (p. 1 of 11) |
< Previous Next >
|
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
We start by internalizing five standard logical connectives: {ganai}, {ge}, {go}, {ga}, and {gonai}. We will use these connectives to provide a basic logical framework for defining selbri and proving bridi. | ||
Before logic, we must define some basic elements of syntax: bridi, selbri, and sumti. We will also embrace some experimental concepts not named in the baseline valsi, but exposed in the baseline grammar: prenexes and bridi-tails. | ||
Syntax | tsb 1 | Any selbri is a valid brirebla. |
brirebla bu'a | ||
Syntax | tss 2 | Any brirebla can have an additional trailing sumti. |
brirebla bo'a ko'a | ||
Syntax | btb 3 | Build a bridi from a sumti and brirebla. |
bridi ko'a bo'a | ||
Theorem | bu 4 | Normal form for unary selbri. (Contributed by la korvo, 14-Aug-2023.) |
bridi ko'a bu'a | ||
Theorem | bb 5 | Normal form for binary selbri. (Contributed by la korvo, 14-Aug-2023.) |
bridi ko'a bu'a ko'e | ||
Theorem | bt 6 | Normal form for ternary selbri. (Contributed by la korvo, 14-Aug-2023.) |
bridi ko'a bu'a ko'e ko'i | ||
Theorem | bq 7 | Normal form for quaternary selbri. (Contributed by la korvo, 19-Mar-2024.) |
bridi ko'a bu'a ko'e ko'i ko'o | ||
Theorem | bp 8 | Normal form for quinary selbri. To avoid conflict with bq 7 this syntax is "bp" for "bridi pentad". (Contributed by la korvo, 22-Jun-2024.) |
bridi ko'a bu'a ko'e ko'i ko'o ko'u | ||
We start with the most fundamental connective, {ganai}, which denotes implication. We will build combinators from the SK basis, which is universal over parametric combinators. This gives us both an enormous degree of flexibility, because we may build any well-typed combinator, as well as confidence in correctness, because the SK basis is well-studied. We also require a single inference-building rule, ax-mp 10. In terms of category theory, {ganai broda gi brode} is an arrow in a syntactic category of equivalence classes of bridi, and the bridi {broda} and {brode} are objects. Note that, since we are using metavariables to denote bridi, we automatically denote equivalence classes. | ||
Syntax | bgan 9 | If {broda} and {brode} are bridi, then so is {ganai broda gi brode}. In terms of category theory, our category of bridi is closed. |
bridi ganai broda gi brode | ||
Axiom | ax-mp 10 | Because {ganai} encodes a syllogism, it may be eliminated by modus ponens. In terms of categorical logic, {broda} implies {brode} and {broda} is assumed. |
⊢ broda ![]() ![]() | ||
Axiom | ax-k 11 | The principle of simplification. Known as the constant combinator, or K, in combinator calculus. |
⊢ ganai broda gi ganai brode gi broda | ||
Theorem | ki 12 | Inference form of ax-k 11 (Contributed by la korvo, 27-Jul-2023.) |
⊢ broda ![]() | ||
Theorem | mpki 13 | Discharge a proven antecedent and replace it with another one. (Contributed by la korvo, 4-Jan-2025.) |
⊢ broda ![]() ![]() | ||
Theorem | kii 14 | Inference form of ki 12 (Contributed by la korvo, 27-Jul-2023.) |
⊢ broda ![]() ![]() | ||
Axiom | ax-s 15 | Frege's axiom. Known as the S combinator in combinator calculus. |
⊢ ganai ganai broda gi ganai brode gi brodi gi ganai ganai broda gi brode gi ganai broda gi brodi | ||
Theorem | si 16 | Inference form of ax-s 15 (Contributed by la korvo, 27-Jul-2023.) |
⊢ ganai broda gi ganai brode gi brodi ![]() | ||
Theorem | ganai-comp-rli 17 | Lift an implication to have a common antecedent as an environment. Right-to-left composition of arrows. (Contributed by la korvo, 8-Jul-2025.) |
⊢ ganai broda gi brode ![]() | ||
Theorem | mpd 18 | Deductive form of ax-mp 10 (Contributed by la korvo, 27-Jul-2023.) |
⊢ ganai broda gi brode ![]() ![]() | ||
Theorem | id 19 | The principle of identity. This is distantly related to, but not the same as, the identity relation df-du 251. In terms of category theory, this proves that identity arrows exist. (Contributed by la korvo, 27-Jul-2023.) |
⊢ ganai broda gi broda | ||
Theorem | idd 20 | Deduction form of id 19 (Contributed by la korvo, 4-Jan-2025.) |
⊢ ganai broda gi ganai brode gi brode | ||
Theorem | syl 21 | The quintessential syllogism. This inference is a standard workhorse for producing deductive forms. In terms of category theory, it composes arrows. (Contributed by la korvo, 30-Jul-2023.) |
⊢ ganai broda gi brode ![]() ![]() | ||
Theorem | sd 22 | Deductive form of ax-s 15 (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai broda gi ganai brode gi ganai brodi gi brodo ![]() | ||
Theorem | mpdd 23 | Nested form of mpd 18 (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai broda gi ganai brode gi brodi ![]() ![]() | ||
Theorem | sylcom 24 | A syllogism which shuffles antecedents. (Contributed by la korvo, 30-Jul-2023.) |
⊢ ganai broda gi ganai brode gi brodi ![]() ![]() | ||
Theorem | syl6 25 | A syllogism replacing consequents. (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai broda gi ganai brode gi brodi ![]() ![]() | ||
Theorem | syl6c 26 | A contractive variant of syl6 25 (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai broda gi ganai brode gi brodi ![]() ![]() ![]() | ||
Theorem | kd 27 | Deductive form of ax-k 11 (Contributed by la korvo, 30-Jul-2023.) |
⊢ ganai broda gi brode ![]() | ||
Theorem | syl5com 28 | A syllogism which shuffles antecedents. (Contributed by la korvo, 30-Jul-2023.) |
⊢ ganai broda gi brode ![]() ![]() | ||
Theorem | ganai-swap12 29 | Naturally swap the first and second antecedents in an internalized inference. (Contributed by la korvo, 30-Jul-2023.) |
⊢ ganai broda gi ganai brode gi brodi ![]() | ||
Theorem | mpcom 30 | Remove a duplicated antecedent from an inference. (Contributed by la korvo, 8-Jul-2025.) |
⊢ ganai broda gi brode ![]() ![]() | ||
Theorem | mpc 31 | A closed version of ax-mp 10 (Contributed by la korvo, 1-Jan-2025.) |
⊢ ganai broda gi ganai ganai broda gi brode gi brode | ||
Theorem | syl5 32 | A syllogism which shuffles antecedents. (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai broda gi brode ![]() ![]() | ||
Theorem | syl2im 33 | Replace two antecedents in parallel. (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai broda gi brode ![]() ![]() ![]() | ||
Theorem | ganai-abs 34 | Absorb a redundant antecedent. (Contributed by la korvo, 30-Jul-2023.) |
⊢ ganai broda gi ganai broda gi brode ![]() | ||
Theorem | sylc 35 | A contracting syllogism. (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai broda gi brode ![]() ![]() ![]() | ||
Theorem | mpi 36 | A nested modus ponens. (Contributed by la korvo, 27-Jul-2023.) |
⊢ broda ![]() ![]() | ||
Theorem | mp2 37 | Double modus ponens. (Contributed by la korvo, 27-Jul-2023.) |
⊢ broda ![]() ![]() ![]() | ||
Theorem | ganai-comp-rld 38 | A deduction form of right-to-left composition. (Contributed by la korvo, 1-Jan-2025.) |
⊢ ganai broda gi ganai brode gi brodi ![]() | ||
Theorem | ganai-comp-rl 39 | A closed syllogism. Categorically, this is the internal version of composition, using the traditional right-to-left ordering. (Contributed by la korvo, 1-Jan-2025.) |
⊢ ganai ganai broda gi brode gi ganai ganai brodi gi broda gi ganai brodi gi brode | ||
Theorem | syldd 40 | Deduction form of syld (future) (Contributed by la korvo, 1-Jan-2025.) |
⊢ ganai broda gi ganai brode gi ganai brodi gi brodo ![]() ![]() | ||
Theorem | syl5d 41 | Deduction form of syl5 32 (Contributed by la korvo, 1-Jan-2025.) |
⊢ ganai broda gi ganai brode gi brodi ![]() ![]() | ||
Theorem | syl9 42 | A syllogism. (Contributed by la korvo, 1-Jan-2025.) |
⊢ ganai broda gi ganai brode gi brodi ![]() ![]() | ||
Theorem | ganai-swap23 43 | Naturally swap the second and third antecedents in an internalized inference. (Contributed by la korvo, 30-Jul-2023.) |
⊢ ganai broda gi ganai brode gi ganai brodi gi brodo ![]() | ||
Theorem | imim12d 44 | A deduction interleaving two implications. (Contributed by la korvo, 15-Jul-2025.) |
⊢ ganai broda gi ganai brode gi brodi ![]() ![]() | ||
Theorem | ganai-comp-lrd 45 | Deductive form of left-to-right composition. (Contributed by la korvo, 15-Jul-2025.) |
⊢ ganai broda gi ganai brode gi brodi ![]() | ||
Theorem | ganai-comp-lr 46 | Internalized version of left-to-right composition. (Contributed by la korvo, 15-Jul-2025.) |
⊢ ganai ganai broda gi brode gi ganai ganai brode gi brodi gi ganai broda gi brodi | ||
Syntax | bge 47 |
|
bridi ge broda gi brode | ||
Axiom | ax-ge-le 48 | Elimination of {ge} on the left. Curry of the left-hand projection. |
⊢ ganai ge broda gi brode gi broda | ||
Axiom | ax-ge-re 49 |
Elimination of {ge} on the right. Curry of the right-hand
projection.
|
⊢ ganai ge broda gi brode gi brode | ||
Axiom | ax-ge-in 50 | Introduction of {ge}. Curry of the I combinator. |
⊢ ganai broda gi ganai brode gi ge broda gi brode | ||
Theorem | ge-lei 51 | Inference form of ax-ge-le 48 (Contributed by la korvo, 27-Jul-2023.) |
⊢ ge broda gi brode ![]() | ||
Theorem | ge-led 52 | Deductive form of ax-ge-le 48 (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai broda gi ge brode gi brodi ![]() | ||
Theorem | ge-rei 53 | Inference form of ax-ge-re 49 (Contributed by la korvo, 27-Jul-2023.) |
⊢ ge broda gi brode ![]() | ||
Theorem | ge-red 54 | Deductive form of ax-ge-re 49 (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai broda gi ge brode gi brodi ![]() | ||
Theorem | ge-ini 55 | Inference form of ax-ge-in 50 (Contributed by la korvo, 27-Jul-2023.) |
⊢ broda ![]() ![]() | ||
Theorem | ancl 56 | Internalization of product comonads. (Contributed by la korvo, 8-Jul-2025.) |
⊢ ganai ganai broda gi brode gi ganai broda gi ge broda gi brode | ||
Theorem | ge-ganai 57 | Conjunction implies implication. (Contributed by la korvo, 22-Jun-2024.) |
⊢ ganai ge broda gi brode gi ganai broda gi brode | ||
Theorem | ge-in-swap12 58 | ax-ge-in 50 with swapped antecedents. (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai broda gi ganai brode gi ge brode gi broda | ||
Theorem | cur 59 | The natural curry (or "import") for any well-formed statement. (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai broda gi ganai brode gi brodi ![]() | ||
Theorem | cur-swap12 60 | cur 59 with swapped antecedents. (Contributed by la korvo, 8-Jul-2025.) |
⊢ ganai broda gi ganai brode gi brodi ![]() | ||
Theorem | uncur 61 | The natural uncurry (or "export") for any well-formed statement. (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai
ge broda gi brode gi brodi ![]() | ||
Theorem | uncur-swap12 62 | uncur 61 with swapped antecedents. (Contributed by la korvo, 8-Jul-2025.) |
⊢ ganai
ge broda gi brode gi brodi ![]() | ||
Theorem | weakar 63 | Weaken an antecedent on the right. (Contributed by la korvo, 9-Jul-2025.) |
⊢ ganai broda gi brode ![]() | ||
Theorem | weakard 64 | Deduction form of weakar 63 (Contributed by la korvo, 9-Jul-2025.) |
⊢ ganai broda gi ganai brode gi brodi ![]() | ||
Theorem | answap 65 | Swap antecedents. (Contributed by la korvo, 9-Jul-2025.) |
⊢ ganai
ge broda gi brode gi brodi ![]() | ||
Theorem | syldan 66 | A syllogism flattening a nested pair. (Contributed by la korvo, 9-Jul-2025.) |
⊢ ganai
ge broda gi brode gi brodi ![]() ![]() | ||
Theorem | weakal 67 | Weaken an antecedent on the left. (Contributed by la korvo, 9-Jul-2025.) |
⊢ ganai broda gi brode ![]() | ||
Theorem | sylan2 68 | A syllogism weakening the antecedent. (Contributed by la korvo, 9-Jul-2025.) |
⊢ ganai broda gi brodi ![]() ![]() | ||
Theorem | ge-prod 69 | All binary products exist. (Contributed by la korvo, 22-Jun-2024.) |
⊢ ganai broda gi brode ![]() ![]() | ||
Theorem | syl2anc 70 | A contracting syllogism. (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai broda gi brode ![]() ![]() ![]() | ||
Theorem | mpancom 71 | A variant of mpan 73 (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai broda gi brode ![]() ![]() | ||
Theorem | mpdan 72 | A variant of mpan 73 (Contributed by la korvo, 8-Jul-2025.) |
⊢ ganai broda gi brode ![]() ![]() | ||
Theorem | mpan 73 | An inference eliminating a conjunction from the antecedent. (Contributed by la korvo, 31-Jul-2023.) |
⊢ broda ![]() ![]() | ||
Theorem | mpan2 74 | An inference eliminating a conjunction from the antecedent. (Contributed by la korvo, 8-Jul-2025.) |
⊢ brode ![]() ![]() | ||
Theorem | mp2an 75 | An inference eliminating a conjunction from the antecedent. (Contributed by la korvo, 31-Jul-2023.) |
⊢ broda ![]() ![]() ![]() | ||
Theorem | mpan9 76 | An inference. (Contributed by la korvo, 9-Jul-2025.) |
⊢ ganai broda gi brode ![]() ![]() | ||
Theorem | sylan 77 | A syllogism refining a conjunction. (Contributed by la korvo, 9-Jul-2025.) |
⊢ ganai broda gi brode ![]() ![]() | ||
Theorem | syl2an 78 | A double syllogism. (Contributed by la korvo, 9-Jul-2025.) |
⊢ ganai broda gi brode ![]() ![]() ![]() | ||
Theorem | ge-pair 79 | A universal property of products: given two arrows in Loj, there is an arrow from the product of their sources to the product of their targets. (Contributed by la korvo, 9-Jul-2025.) |
⊢ ganai broda gi brode ![]() ![]() | ||
Theorem | ge-pairl 80 | ge-pair 79 with only one implication, on the left. (Contributed by la korvo, 9-Jul-2025.) |
⊢ ganai broda gi brode ![]() | ||
Theorem | ge-pairr 81 | ge-pair 79 with only one implication, on the right. (Contributed by la korvo, 9-Jul-2025.) |
⊢ ganai broda gi brode ![]() | ||
Syntax | bgo 82 | If {broda} and {brode} are bridi, then so is {go broda gi brode}. |
bridi go broda gi brode | ||
Definition | df-go 83 | Definition of {go} in terms of {ganai} and {ge}. This is the standard definition of the biconditional connective in higher-order intuitionistic logic. This can be justified intuitionistically; see theorem df-bi along with bijust from [ILE] p. 0. |
⊢ ge ganai go broda gi brode gi ge ganai broda gi brode gi ganai brode gi broda gi ganai ge ganai broda gi brode gi ganai brode gi broda gi go broda gi brode | ||
Theorem | goli 84 | Inference form of left side of df-go 83 (Contributed by la korvo, 29-Jul-2023.) |
⊢ go broda gi brode ![]() | ||
Theorem | go-ganai 85 | Biconditional implication may be weakened to unidirectional implication. Category-theoretically, this theorem embeds the core of Loj. Inference form of left side of goli 84. (Contributed by la korvo, 17-Jul-2023.) (Shortened by la korvo, 29-Jul-2023.) |
⊢ go broda gi brode ![]() | ||
Theorem | gori 86 | Inference form of right side of df-go 83 (Contributed by la korvo, 30-Jul-2023.) |
⊢ ge
ganai broda gi brode gi ganai brode gi broda ![]() | ||
Theorem | iso 87 | Inference form of right side of gori 86 (Contributed by la korvo, 30-Jul-2023.) |
⊢ ganai broda gi brode ![]() ![]() | ||
Theorem | bi1 88 | Property of biconditionals. (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai go broda gi brode gi ganai broda gi brode | ||
Theorem | bi2 89 | Property of biconditionals. (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai go broda gi brode gi ganai brode gi broda | ||
Theorem | bi3 90 | Property of biconditionals. (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai ganai broda gi brode gi ganai ganai brode gi broda gi go broda gi brode | ||
Theorem | go-ganaid 91 | Deduction form of go-ganai 85 (Contributed by la korvo, 4-Jan-2025.) |
⊢ ganai broda gi go brode gi brodi ![]() | ||
Theorem | isodd 92 | Double deduction form of iso 87 (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai broda gi ganai brode gi ganai brodi gi brodo ![]() ![]() | ||
Theorem | isod-lem 93 | Lemma for isod 94 known as theorem impbid21d in [ILE] p. 0. (Contributed by la korvo, 31-Jul-2023.) [Auxiliary lemma - not displayed.] |
Theorem | isod 94 | Deduction form of iso 87 (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai broda gi ganai brode gi brodi ![]() ![]() | ||
Theorem | go-id 95 | {go} is reflexive. (Contributed by la korvo, 30-Jul-2023.) |
⊢ go broda gi broda | ||
Theorem | go-com-lem 96 | Lemma: {go} commutes in one direction. (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai go broda gi brode gi go brode gi broda | ||
Theorem | go-com 97 | {go} commutes. (Contributed by la korvo, 17-Aug-2023.) |
⊢ go go broda gi brode gi go brode gi broda | ||
Theorem | go-comi 98 | Inference form of go-com 97 (Contributed by la korvo, 31-Jul-2023.) |
⊢ go broda gi brode ![]() | ||
Axiom | ax-go-trans 99 | {go} is transitive. |
⊢ go broda gi brode ![]() ![]() | ||
Theorem | go-syl 100 | {go} admits composition. (Contributed by la korvo, 16-Aug-2023.) |
⊢ go broda gi brode ![]() ![]() |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |