P. 1 of Theorem List - brismu bridi

Home	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)
Type	Label	Description
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.

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

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.

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 ⊢ ganai broda gi brode ⊢ brode

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 ⊢ ganai brode gi broda

Theorem	mpki 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

Theorem	kii 14	Inference form of ki 12 (Contributed by la korvo, 27-Jul-2023.)
⊢ broda ⊢ brode ⊢ 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 ⊢ ganai ganai broda gi brode gi ganai broda 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 ⊢ ganai ganai brodi gi broda gi ganai brodi gi brode

Theorem	mpd 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

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 ⊢ ganai brode gi brodi ⊢ ganai broda gi brodi

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 ⊢ ganai broda gi ganai ganai brode gi brodi gi ganai brode gi brodo

Theorem	mpdd 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

Theorem	sylcom 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

Theorem	syl6 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

Theorem	syl6c 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

Theorem	kd 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

Theorem	syl5com 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

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 ⊢ ganai brode gi ganai broda gi brodi

Theorem	mpcom 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

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 ⊢ ganai brodi gi ganai brode gi brodo ⊢ ganai brodi gi ganai broda gi brodo

Theorem	syl2im 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

Theorem	ganai-abs 34	Absorb a redundant antecedent. (Contributed by la korvo, 30-Jul-2023.)
⊢ ganai broda gi ganai broda gi brode ⊢ ganai broda gi brode

Theorem	sylc 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

Theorem	mpi 36	A nested modus ponens. (Contributed by la korvo, 27-Jul-2023.)
⊢ broda ⊢ ganai brode gi ganai broda gi brodi ⊢ ganai brode gi brodi

Theorem	mp2 37	Double modus ponens. (Contributed by la korvo, 27-Jul-2023.)
⊢ broda ⊢ brode ⊢ ganai broda gi ganai brode gi brodi ⊢ brodi

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 ⊢ ganai broda gi ganai ganai brodo gi brode gi ganai brodo 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 ⊢ ganai broda gi ganai brode gi ganai brodo gi brodu ⊢ ganai broda gi ganai brode gi ganai brodi gi brodu

Theorem	syl5d 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

Theorem	syl9 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

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 ⊢ ganai broda gi ganai brodi gi ganai brode gi brodo

Theorem	imim12d 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

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 ⊢ ganai broda gi ganai ganai brodi gi brodo gi ganai brode gi brodo

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

1.3 Conjunctions I: {ge}

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 ⊢ broda

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 ⊢ ganai broda gi brode

Theorem	ge-rei 53	Inference form of ax-ge-re 49 (Contributed by la korvo, 27-Jul-2023.)
⊢ ge broda gi brode ⊢ 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 ⊢ ganai broda gi brodi

Theorem	ge-ini 55	Inference form of ax-ge-in 50 (Contributed by la korvo, 27-Jul-2023.)
⊢ broda ⊢ brode ⊢ ge broda gi brode

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 ⊢ ganai ge broda gi 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 ⊢ ganai ge brode gi broda 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 ⊢ ganai broda gi ganai 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 ⊢ ganai brode gi ganai broda gi brodi

Theorem	weakar 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

Theorem	weakard 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

Theorem	answap 65	Swap antecedents. (Contributed by la korvo, 9-Jul-2025.)
⊢ ganai ge broda gi brode gi brodi ⊢ ganai ge brode gi broda 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 ⊢ ganai ge broda gi brodi gi brodo ⊢ ganai ge broda gi brode gi brodo

Theorem	weakal 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

Theorem	sylan2 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

Theorem	ge-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

Theorem	syl2anc 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

Theorem	mpancom 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

Theorem	mpdan 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

Theorem	mpan 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

Theorem	mpan2 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

Theorem	mp2an 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

Theorem	mpan9 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

Theorem	sylan 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

Theorem	syl2an 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

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 ⊢ ganai brodi gi brodo ⊢ ganai ge broda gi brodi gi ge brode gi brodo

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 ⊢ ganai ge broda gi brodi gi ge brode gi brodi

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 ⊢ ganai ge brodi gi broda gi ge brodi gi brode

1.4 Biconditionals I: {go}

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 ⊢ ge ganai broda gi brode gi ganai brode gi broda

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 ⊢ ganai 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 ⊢ go broda gi brode

Theorem	iso 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

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 ⊢ ganai broda gi ganai 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 ⊢ ganai broda gi ganai brode gi ganai brodo gi brodi ⊢ ganai broda gi ganai brode gi go 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 ⊢ ganai broda gi ganai brodi gi brode ⊢ ganai broda gi go 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 ⊢ go brode gi broda

Axiom	ax-go-trans 99	{go} is transitive.
⊢ go broda gi brode ⊢ go brode gi brodi ⊢ go broda gi brodi

Theorem	go-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

< Previous Next >