HomeHome brismu bridi
Theorem List (p. 1 of 11)
< Previous  Next >

Mirrors  >  Metamath Home Page  >  Home Page  >  Theorem List Contents       This page: Page List

Theorem List for brismu bridi - 1-100   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
PART 1  LOGICAL CONNECTIVES

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.

 
1.1  Basic syntax

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.

 
Syntaxtsb 1 Any selbri is a valid brirebla.
brirebla bu'a
 
Syntaxtss 2 Any brirebla can have an additional trailing sumti.
brirebla bo'a ko'a
 
Syntaxbtb 3 Build a bridi from a sumti and brirebla.
bridi ko'a bo'a
 
Theorembu 4 Normal form for unary selbri. (Contributed by la korvo, 14-Aug-2023.)
bridi ko'a bu'a
 
Theorembb 5 Normal form for binary selbri. (Contributed by la korvo, 14-Aug-2023.)
bridi ko'a bu'a ko'e
 
Theorembt 6 Normal form for ternary selbri. (Contributed by la korvo, 14-Aug-2023.)
bridi ko'a bu'a ko'e ko'i
 
Theorembq 7 Normal form for quaternary selbri. (Contributed by la korvo, 19-Mar-2024.)
bridi ko'a bu'a ko'e ko'i ko'o
 
Theorembp 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
 
1.2  Implication I: {ganai}

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.

 
Syntaxbgan 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
 
Axiomax-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   &   ⊢ ganai broda gi brode   =>   ⊢ brode
 
Axiomax-k 11 The principle of simplification. Known as the constant combinator, or K, in combinator calculus.
ganai broda gi ganai brode gi broda
 
Theoremki 12 Inference form of ax-k 11 (Contributed by la korvo, 27-Jul-2023.)
broda   =>   ⊢ ganai brode gi broda
 
Theoremmpki 13 Discharge a proven antecedent and replace it with another one. (Contributed by la korvo, 4-Jan-2025.)
broda   &   ⊢ ganai broda gi brode   =>   ⊢ ganai brodi gi brode
 
Theoremkii 14 Inference form of ki 12 (Contributed by la korvo, 27-Jul-2023.)
broda   &   ⊢ brode   =>   ⊢ broda
 
Axiomax-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
 
Theoremsi 16 Inference form of ax-s 15 (Contributed by la korvo, 27-Jul-2023.)
ganai broda gi ganai brode gi brodi   =>   ⊢ ganai ganai broda gi brode gi ganai broda gi brodi
 
Theoremganai-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   =>   ⊢ ganai ganai brodi gi broda gi ganai brodi gi brode
 
Theoremmpd 18 Deductive form of ax-mp 10 (Contributed by la korvo, 27-Jul-2023.)
ganai broda gi brode   &   ⊢ ganai broda gi ganai brode gi brodi   =>   ⊢ ganai broda gi brodi
 
Theoremid 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
 
Theoremidd 20 Deduction form of id 19 (Contributed by la korvo, 4-Jan-2025.)
ganai broda gi ganai brode gi brode
 
Theoremsyl 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   &   ⊢ ganai brode gi brodi   =>   ⊢ ganai broda gi brodi
 
Theoremsd 22 Deductive form of ax-s 15 (Contributed by la korvo, 31-Jul-2023.)
ganai broda gi ganai brode gi ganai brodi gi brodo   =>   ⊢ ganai broda gi ganai ganai brode gi brodi gi ganai brode gi brodo
 
Theoremmpdd 23 Nested form of mpd 18 (Contributed by la korvo, 31-Jul-2023.)
ganai broda gi ganai brode gi brodi   &   ⊢ ganai broda gi ganai brode gi ganai brodi gi brodo   =>   ⊢ ganai broda gi ganai brode gi brodo
 
Theoremsylcom 24 A syllogism which shuffles antecedents. (Contributed by la korvo, 30-Jul-2023.)
ganai broda gi ganai brode gi brodi   &   ⊢ ganai brode gi ganai brodi gi brodo   =>   ⊢ ganai broda gi ganai brode gi brodo
 
Theoremsyl6 25 A syllogism replacing consequents. (Contributed by la korvo, 31-Jul-2023.)
ganai broda gi ganai brode gi brodi   &   ⊢ ganai brodi gi brodo   =>   ⊢ ganai broda gi ganai brode gi brodo
 
Theoremsyl6c 26 A contractive variant of syl6 25 (Contributed by la korvo, 31-Jul-2023.)
ganai broda gi ganai brode gi brodi   &   ⊢ ganai broda gi ganai brode gi brodo   &   ⊢ ganai brodi gi ganai brodo gi brodu   =>   ⊢ ganai broda gi ganai brode gi brodu
 
Theoremkd 27 Deductive form of ax-k 11 (Contributed by la korvo, 30-Jul-2023.)
ganai broda gi brode   =>   ⊢ ganai broda gi ganai brodi gi brode
 
Theoremsyl5com 28 A syllogism which shuffles antecedents. (Contributed by la korvo, 30-Jul-2023.)
ganai broda gi brode   &   ⊢ ganai brodi gi ganai brode gi brodo   =>   ⊢ ganai broda gi ganai brodi gi brodo
 
Theoremganai-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   =>   ⊢ ganai brode gi ganai broda gi brodi
 
Theoremmpcom 30 Remove a duplicated antecedent from an inference. (Contributed by la korvo, 8-Jul-2025.)
ganai broda gi brode   &   ⊢ ganai brode gi ganai broda gi brodi   =>   ⊢ ganai broda gi brodi
 
Theoremmpc 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
 
Theoremsyl5 32 A syllogism which shuffles antecedents. (Contributed by la korvo, 31-Jul-2023.)
ganai broda gi brode   &   ⊢ ganai brodi gi ganai brode gi brodo   =>   ⊢ ganai brodi gi ganai broda gi brodo
 
Theoremsyl2im 33 Replace two antecedents in parallel. (Contributed by la korvo, 31-Jul-2023.)
ganai broda gi brode   &   ⊢ ganai brodi gi brodo   &   ⊢ ganai brode gi ganai brodo gi brodu   =>   ⊢ ganai broda gi ganai brodi gi brodu
 
Theoremganai-abs 34 Absorb a redundant antecedent. (Contributed by la korvo, 30-Jul-2023.)
ganai broda gi ganai broda gi brode   =>   ⊢ ganai broda gi brode
 
Theoremsylc 35 A contracting syllogism. (Contributed by la korvo, 31-Jul-2023.)
ganai broda gi brode   &   ⊢ ganai broda gi brodi   &   ⊢ ganai brode gi ganai brodi gi brodo   =>   ⊢ ganai broda gi brodo
 
Theoremmpi 36 A nested modus ponens. (Contributed by la korvo, 27-Jul-2023.)
broda   &   ⊢ ganai brode gi ganai broda gi brodi   =>   ⊢ ganai brode gi brodi
 
Theoremmp2 37 Double modus ponens. (Contributed by la korvo, 27-Jul-2023.)
broda   &   ⊢ brode   &   ⊢ ganai broda gi ganai brode gi brodi   =>   ⊢ brodi
 
Theoremganai-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   =>   ⊢ ganai broda gi ganai ganai brodo gi brode gi ganai brodo gi brodi
 
Theoremganai-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
 
Theoremsyldd 40 Deduction form of syld (future) (Contributed by la korvo, 1-Jan-2025.)
ganai broda gi ganai brode gi ganai brodi gi brodo   &   ⊢ ganai broda gi ganai brode gi ganai brodo gi brodu   =>   ⊢ ganai broda gi ganai brode gi ganai brodi gi brodu
 
Theoremsyl5d 41 Deduction form of syl5 32 (Contributed by la korvo, 1-Jan-2025.)
ganai broda gi ganai brode gi brodi   &   ⊢ ganai broda gi ganai brodo gi ganai brodi gi brodu   =>   ⊢ ganai broda gi ganai brodo gi ganai brode gi brodu
 
Theoremsyl9 42 A syllogism. (Contributed by la korvo, 1-Jan-2025.)
ganai broda gi ganai brode gi brodi   &   ⊢ ganai brodo gi ganai brodi gi brodu   =>   ⊢ ganai broda gi ganai brodo gi ganai brode gi brodu
 
Theoremganai-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   =>   ⊢ ganai broda gi ganai brodi gi ganai brode gi brodo
 
Theoremimim12d 44 A deduction interleaving two implications. (Contributed by la korvo, 15-Jul-2025.)
ganai broda gi ganai brode gi brodi   &   ⊢ ganai broda gi ganai brodo gi brodu   =>   ⊢ ganai broda gi ganai ganai brodi gi brodo gi ganai brode gi brodu
 
Theoremganai-comp-lrd 45 Deductive form of left-to-right composition. (Contributed by la korvo, 15-Jul-2025.)
ganai broda gi ganai brode gi brodi   =>   ⊢ ganai broda gi ganai ganai brodi gi brodo gi ganai brode gi brodo
 
Theoremganai-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
 
1.3  Conjunctions I: {ge}
 
Syntaxbge 47

bridi ge broda gi brode
 
Axiomax-ge-le 48 Elimination of {ge} on the left. Curry of the left-hand projection.
ganai ge broda gi brode gi broda
 
Axiomax-ge-re 49 Elimination of {ge} on the right. Curry of the right-hand projection.

ganai ge broda gi brode gi brode
 
Axiomax-ge-in 50 Introduction of {ge}. Curry of the I combinator.
ganai broda gi ganai brode gi ge broda gi brode
 
Theoremge-lei 51 Inference form of ax-ge-le 48 (Contributed by la korvo, 27-Jul-2023.)
ge broda gi brode   =>   ⊢ broda
 
Theoremge-led 52 Deductive form of ax-ge-le 48 (Contributed by la korvo, 31-Jul-2023.)
ganai broda gi ge brode gi brodi   =>   ⊢ ganai broda gi brode
 
Theoremge-rei 53 Inference form of ax-ge-re 49 (Contributed by la korvo, 27-Jul-2023.)
ge broda gi brode   =>   ⊢ brode
 
Theoremge-red 54 Deductive form of ax-ge-re 49 (Contributed by la korvo, 31-Jul-2023.)
ganai broda gi ge brode gi brodi   =>   ⊢ ganai broda gi brodi
 
Theoremge-ini 55 Inference form of ax-ge-in 50 (Contributed by la korvo, 27-Jul-2023.)
broda   &   ⊢ brode   =>   ⊢ ge broda gi brode
 
Theoremancl 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
 
Theoremge-ganai 57 Conjunction implies implication. (Contributed by la korvo, 22-Jun-2024.)
ganai ge broda gi brode gi ganai broda gi brode
 
Theoremge-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
 
Theoremcur 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   =>   ⊢ ganai ge broda gi brode gi brodi
 
Theoremcur-swap12 60 cur 59 with swapped antecedents. (Contributed by la korvo, 8-Jul-2025.)
ganai broda gi ganai brode gi brodi   =>   ⊢ ganai ge brode gi broda gi brodi
 
Theoremuncur 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   =>   ⊢ ganai broda gi ganai brode gi brodi
 
Theoremuncur-swap12 62 uncur 61 with swapped antecedents. (Contributed by la korvo, 8-Jul-2025.)
ganai ge broda gi brode gi brodi   =>   ⊢ ganai brode gi ganai broda gi brodi
 
Theoremweakar 63 Weaken an antecedent on the right. (Contributed by la korvo, 9-Jul-2025.)
ganai broda gi brode   =>   ⊢ ganai ge broda gi brodi gi brode
 
Theoremweakard 64 Deduction form of weakar 63 (Contributed by la korvo, 9-Jul-2025.)
ganai broda gi ganai brode gi brodi   =>   ⊢ ganai broda gi ganai ge brode gi brodo gi brodi
 
Theoremanswap 65 Swap antecedents. (Contributed by la korvo, 9-Jul-2025.)
ganai ge broda gi brode gi brodi   =>   ⊢ ganai ge brode gi broda gi brodi
 
Theoremsyldan 66 A syllogism flattening a nested pair. (Contributed by la korvo, 9-Jul-2025.)
ganai ge broda gi brode gi brodi   &   ⊢ ganai ge broda gi brodi gi brodo   =>   ⊢ ganai ge broda gi brode gi brodo
 
Theoremweakal 67 Weaken an antecedent on the left. (Contributed by la korvo, 9-Jul-2025.)
ganai broda gi brode   =>   ⊢ ganai ge brodi gi broda gi brode
 
Theoremsylan2 68 A syllogism weakening the antecedent. (Contributed by la korvo, 9-Jul-2025.)
ganai broda gi brodi   &   ⊢ ganai ge brode gi brodi gi brodo   =>   ⊢ ganai ge brode gi broda gi brodo
 
Theoremge-prod 69 All binary products exist. (Contributed by la korvo, 22-Jun-2024.)
ganai broda gi brode   &   ⊢ ganai broda gi brodi   =>   ⊢ ganai broda gi ge brode gi brodi
 
Theoremsyl2anc 70 A contracting syllogism. (Contributed by la korvo, 31-Jul-2023.)
ganai broda gi brode   &   ⊢ ganai broda gi brodi   &   ⊢ ganai ge brode gi brodi gi brodo   =>   ⊢ ganai broda gi brodo
 
Theoremmpancom 71 A variant of mpan 73 (Contributed by la korvo, 31-Jul-2023.)
ganai broda gi brode   &   ⊢ ganai ge brode gi broda gi brodi   =>   ⊢ ganai broda gi brodi
 
Theoremmpdan 72 A variant of mpan 73 (Contributed by la korvo, 8-Jul-2025.)
ganai broda gi brode   &   ⊢ ganai ge broda gi brode gi brodi   =>   ⊢ ganai broda gi brodi
 
Theoremmpan 73 An inference eliminating a conjunction from the antecedent. (Contributed by la korvo, 31-Jul-2023.)
broda   &   ⊢ ganai ge broda gi brode gi brodi   =>   ⊢ ganai brode gi brodi
 
Theoremmpan2 74 An inference eliminating a conjunction from the antecedent. (Contributed by la korvo, 8-Jul-2025.)
brode   &   ⊢ ganai ge broda gi brode gi brodi   =>   ⊢ ganai broda gi brodi
 
Theoremmp2an 75 An inference eliminating a conjunction from the antecedent. (Contributed by la korvo, 31-Jul-2023.)
broda   &   ⊢ brode   &   ⊢ ganai ge broda gi brode gi brodi   =>   ⊢ brodi
 
Theoremmpan9 76 An inference. (Contributed by la korvo, 9-Jul-2025.)
ganai broda gi brode   &   ⊢ ganai brodi gi ganai brode gi brodo   =>   ⊢ ganai ge broda gi brodi gi brodo
 
Theoremsylan 77 A syllogism refining a conjunction. (Contributed by la korvo, 9-Jul-2025.)
ganai broda gi brode   &   ⊢ ganai ge brode gi brodi gi brodo   =>   ⊢ ganai ge broda gi brodi gi brodo
 
Theoremsyl2an 78 A double syllogism. (Contributed by la korvo, 9-Jul-2025.)
ganai broda gi brode   &   ⊢ ganai brodu gi brodi   &   ⊢ ganai ge brode gi brodi gi brodo   =>   ⊢ ganai ge broda gi brodu gi brodo
 
Theoremge-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   &   ⊢ ganai brodi gi brodo   =>   ⊢ ganai ge broda gi brodi gi ge brode gi brodo
 
Theoremge-pairl 80 ge-pair 79 with only one implication, on the left. (Contributed by la korvo, 9-Jul-2025.)
ganai broda gi brode   =>   ⊢ ganai ge broda gi brodi gi ge brode gi brodi
 
Theoremge-pairr 81 ge-pair 79 with only one implication, on the right. (Contributed by la korvo, 9-Jul-2025.)
ganai broda gi brode   =>   ⊢ ganai ge brodi gi broda gi ge brodi gi brode
 
1.4  Biconditionals I: {go}
 
Syntaxbgo 82 If {broda} and {brode} are bridi, then so is {go broda gi brode}.
bridi go broda gi brode
 
Definitiondf-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
 
Theoremgoli 84 Inference form of left side of df-go 83 (Contributed by la korvo, 29-Jul-2023.)
go broda gi brode   =>   ⊢ ge ganai broda gi brode gi ganai brode gi broda
 
Theoremgo-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   =>   ⊢ ganai broda gi brode
 
Theoremgori 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   =>   ⊢ go broda gi brode
 
Theoremiso 87 Inference form of right side of gori 86 (Contributed by la korvo, 30-Jul-2023.)
ganai broda gi brode   &   ⊢ ganai brode gi broda   =>   ⊢ go broda gi brode
 
Theorembi1 88 Property of biconditionals. (Contributed by la korvo, 31-Jul-2023.)
ganai go broda gi brode gi ganai broda gi brode
 
Theorembi2 89 Property of biconditionals. (Contributed by la korvo, 31-Jul-2023.)
ganai go broda gi brode gi ganai brode gi broda
 
Theorembi3 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
 
Theoremgo-ganaid 91 Deduction form of go-ganai 85 (Contributed by la korvo, 4-Jan-2025.)
ganai broda gi go brode gi brodi   =>   ⊢ ganai broda gi ganai brode gi brodi
 
Theoremisodd 92 Double deduction form of iso 87 (Contributed by la korvo, 31-Jul-2023.)
ganai broda gi ganai brode gi ganai brodi gi brodo   &   ⊢ ganai broda gi ganai brode gi ganai brodo gi brodi   =>   ⊢ ganai broda gi ganai brode gi go brodi gi brodo
 
Theoremisod-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.]
 
Theoremisod 94 Deduction form of iso 87 (Contributed by la korvo, 31-Jul-2023.)
ganai broda gi ganai brode gi brodi   &   ⊢ ganai broda gi ganai brodi gi brode   =>   ⊢ ganai broda gi go brode gi brodi
 
Theoremgo-id 95 {go} is reflexive. (Contributed by la korvo, 30-Jul-2023.)
go broda gi broda
 
Theoremgo-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
 
Theoremgo-com 97 {go} commutes. (Contributed by la korvo, 17-Aug-2023.)
go go broda gi brode gi go brode gi broda
 
Theoremgo-comi 98 Inference form of go-com 97 (Contributed by la korvo, 31-Jul-2023.)
go broda gi brode   =>   ⊢ go brode gi broda
 
Axiomax-go-trans 99 {go} is transitive.
go broda gi brode   &   ⊢ go brode gi brodi   =>   ⊢ go broda gi brodi
 
Theoremgo-syl 100 {go} admits composition. (Contributed by la korvo, 16-Aug-2023.)
go broda gi brode   &   ⊢ go brode gi brodi   =>   ⊢ go broda gi brodi
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1048
  Copyright terms: Public domain < Previous  Next >