P. 1 of Theorem List - brismu bridi

Home	brismu bridi Theorem List (p. 1 of 8)	< 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 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. Axiom ax-1 in [ILE] p. 0.
⊢ 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	kii 13	Inference form of ki 12 (Contributed by la korvo, 27-Jul-2023.)
⊢ broda ⊢ brode ⊢ broda

Axiom	ax-s 14	Frege's axiom. Known as the S combinator in combinator calculus. Axiom ax-2 in [ILE] p. 0.
⊢ ganai ganai broda gi ganai brode gi brodi gi ganai ganai broda gi brode gi ganai broda gi brodi

Theorem	si 15	Inference form of ax-s 14 (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	mpd 16	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 17	The principle of identity. This is distantly related to, but not the same as, the identity relation df-du 197. In terms of category theory, this proves that identity arrows exist. (Contributed by la korvo, 27-Jul-2023.)
⊢ ganai broda gi broda

Theorem	syl 18	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 19	Deductive form of ax-s 14 (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 20	Nested form of mpd 16 (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 21	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 22	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 23	A contractive variant of syl6 22 (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 24	Deductive form of ax-k 11 Theorem a1d in [ILE] p. 0. (Contributed by la korvo, 30-Jul-2023.)
⊢ ganai broda gi brode ⊢ ganai broda gi ganai brodi gi brode

Theorem	syl5com 25	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 26	Naturally swap the first and second antecedents in an internalized inference. Theorem com12 in [ILE] p. 0. (Contributed by la korvo, 30-Jul-2023.)
⊢ ganai broda gi ganai brode gi brodi ⊢ ganai brode gi ganai broda gi brodi

Theorem	syl5 27	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 28	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 29	Absorb a redundant antecedent. (Contributed by la korvo, 30-Jul-2023.)
⊢ ganai broda gi ganai broda gi brode ⊢ ganai broda gi brode

Theorem	sylc 30	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 31	A nested modus ponens. Theorem mpi in [ILE] p. 0. (Contributed by la korvo, 27-Jul-2023.)
⊢ broda ⊢ ganai brode gi ganai broda gi brodi ⊢ ganai brode gi brodi

Theorem	mp2 32	Double modus ponens. Theorem mp2 in [ILE] p. 0. (Contributed by la korvo, 27-Jul-2023.)
⊢ broda ⊢ brode ⊢ ganai broda gi ganai brode gi brodi ⊢ brodi

1.3 Conjunctions I: {ge}

Syntax	bge 33
bridi ge broda gi brode

Axiom	ax-ge-le 34	Elimination of {ge} on the left. Curry of the left-hand projection. Axiom ax-ia1 in [ILE] p. 0.
⊢ ganai ge broda gi brode gi broda

Axiom	ax-ge-re 35	Elimination of {ge} on the right. Curry of the right-hand projection. Axiom ax-ia2 in [ILE] p. 0.
⊢ ganai ge broda gi brode gi brode

Axiom	ax-ge-in 36	Introduction of {ge}. Curry of the I combinator. Axiom ax-ia3 in [ILE] p. 0.
⊢ ganai broda gi ganai brode gi ge broda gi brode

Theorem	ge-lei 37	Inference form of ax-ge-le 34 (Contributed by la korvo, 27-Jul-2023.)
⊢ ge broda gi brode ⊢ broda

Theorem	ge-led 38	Deductive form of ax-ge-le 34 (Contributed by la korvo, 31-Jul-2023.)
⊢ ganai broda gi ge brode gi brodi ⊢ ganai broda gi brode

Theorem	ge-rei 39	Inference form of ax-ge-re 35 (Contributed by la korvo, 27-Jul-2023.)
⊢ ge broda gi brode ⊢ brode

Theorem	ge-red 40	Deductive form of ax-ge-re 35 (Contributed by la korvo, 31-Jul-2023.)
⊢ ganai broda gi ge brode gi brodi ⊢ ganai broda gi brodi

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

Theorem	ge-ganai 42	Conjunction implies implication. Theorem pm3.4 in [ILE] p. 0. (Contributed by la korvo, 22-Jun-2024.)
⊢ ganai ge broda gi brode gi ganai broda gi brode

Theorem	ge-in-swap12 43	ax-ge-in 36 with swapped antecedents. (Contributed by la korvo, 31-Jul-2023.)
⊢ ganai broda gi ganai brode gi ge brode gi broda

Theorem	cur 44	The natural curry (or "import") for any well-formed statement. Theorem imp in [ILE] p. 0. (Contributed by la korvo, 31-Jul-2023.)
⊢ ganai broda gi ganai brode gi brodi ⊢ ganai ge broda gi brode gi brodi

Theorem	uncur 45	The natural uncurry (or "export") for any well-formed statement. Theorem ex in [ILE] p. 0. (Contributed by la korvo, 31-Jul-2023.)
⊢ ganai ge broda gi brode gi brodi ⊢ ganai broda gi ganai brode gi brodi

Theorem	jca 46	"Join Consequents with AND". (Contributed by la korvo, 22-Jun-2024.)
⊢ ganai broda gi brode ⊢ ganai broda gi brodi ⊢ ganai broda gi ge brode gi brodi

Theorem	syl2anc 47	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 48	A variant of mpan 49 (Contributed by la korvo, 31-Jul-2023.)
⊢ ganai broda gi brode ⊢ ganai ge brode gi broda gi brodi ⊢ ganai broda gi brodi

Theorem	mpan 49	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	mp2an 50	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

1.4 Biconditionals I: {go}

Syntax	bgo 51	If {broda} and {brode} are bridi, then so is {go broda gi brode}.
bridi go broda gi brode

Definition	df-go 52	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 53	Inference form of left side of df-go 52 (Contributed by la korvo, 29-Jul-2023.)
⊢ go broda gi brode ⊢ ge ganai broda gi brode gi ganai brode gi broda

Theorem	go-ganai 54	Biconditional implication may be weakened to unidirectional implication. Category-theoretically, this theorem embeds the core of Loj. Inference form of left side of goli 53. Theorem biimpi in [ILE] p. 0. (Contributed by la korvo, 17-Jul-2023.) (Shortened by la korvo, 29-Jul-2023.)
⊢ go broda gi brode ⊢ ganai broda gi brode

Theorem	gori 55	Inference form of right side of df-go 52 (Contributed by la korvo, 30-Jul-2023.)
⊢ ge ganai broda gi brode gi ganai brode gi broda ⊢ go broda gi brode

Theorem	iso 56	Inference form of right side of gori 55 (Contributed by la korvo, 30-Jul-2023.)
⊢ ganai broda gi brode ⊢ ganai brode gi broda ⊢ go broda gi brode

Theorem	bi1 57	Property of biconditionals. (Contributed by la korvo, 31-Jul-2023.)
⊢ ganai go broda gi brode gi ganai broda gi brode

Theorem	bi2 58	Property of biconditionals. (Contributed by la korvo, 31-Jul-2023.)
⊢ ganai go broda gi brode gi ganai brode gi broda

Theorem	bi3 59	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	isodd 60	Double deduction form of iso 56 (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 61	Lemma for isod 62 known as theorem impbid21d in [ILE] p. 0. (Contributed by la korvo, 31-Jul-2023.) [Auxiliary lemma - not displayed.]

Theorem	isod 62	Deduction form of iso 56 Theorem impbid in [ILE] p. 0. (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 63	{go} is reflexive. Theorem equid in [ILE] p. 0. (Contributed by la korvo, 30-Jul-2023.)
⊢ go broda gi broda

Theorem	go-com-lem 64	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 65	{go} commutes. (Contributed by la korvo, 17-Aug-2023.)
⊢ go go broda gi brode gi go brode gi broda

Theorem	go-comi 66	Inference form of go-com 65 Theorem bicomi in [ILE] p. 0. (Contributed by la korvo, 31-Jul-2023.)
⊢ go broda gi brode ⊢ go brode gi broda

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

Theorem	go-syl 68	{go} admits composition. (Contributed by la korvo, 16-Aug-2023.)
⊢ go broda gi brode ⊢ go brode gi brodi ⊢ go broda gi brodi

Theorem	bi 69	Like modus ponens ax-mp 10 but for biconditionals. (Contributed by la korvo, 16-Jul-2023.)
⊢ broda ⊢ go broda gi brode ⊢ brode

Theorem	bi-rev 70	Modus ponens in the other direction. Theorem mpbir in [ILE] p. 0. (Contributed by la korvo, 16-Jul-2023.)
⊢ broda ⊢ go brode gi broda ⊢ brode

Theorem	bi-rev-syl 71	The right-hand side of a {go} may also be weakened to a {ganai}. Theorem biimpri in [ILE] p. 0. (Contributed by la korvo, 10-Jul-2023.)
⊢ go broda gi brode ⊢ ganai brode gi broda

Theorem	sylbi 72	Syllogism with a biconditional. (Contributed by la korvo, 25-Jun-2024.)
⊢ go broda gi brode ⊢ ganai brode gi brodi ⊢ ganai broda gi brodi

Theorem	sylib 73	Syllogism with a biconditional. (Contributed by la korvo, 25-Jun-2024.)
⊢ ganai broda gi brode ⊢ go brode gi brodi ⊢ ganai broda gi brodi

Theorem	sylibr 74	Apply a definition to a consequent. Theorem sylibr in [ILE] p. 0. (Contributed by la korvo, 22-Jun-2024.)
⊢ ganai broda gi brode ⊢ go brodi gi brode ⊢ ganai broda gi brodi

Theorem	sylanbrc 75	Deductive unpacking of a definition with conjoined components. Theorem sylanbrc in [ILE] p. 0. (Contributed by la korvo, 22-Jun-2024.)
⊢ ganai broda gi brode ⊢ ganai broda gi brodi ⊢ go brodo gi ge brode gi brodi ⊢ ganai broda gi brodo

Theorem	syl5bi 76	Replace a nested antecedent using a biconditional. (Contributed by la korvo, 22-Jun-2024.)
⊢ go broda gi brode ⊢ ganai brodi gi ganai brode gi brodo ⊢ ganai brodi gi ganai broda gi brodo

1.5 Implication II Unlike the other four connectives, {ganai} is not symmetric. As a result, Lojban's grammar admits both a left-to-right and right-to-left version of each connective for implication.

1.5.1 {na.a}

Syntax	sjnaa 77
sumti ko'a na.a ko'e

Definition	df-na.a 78	Definition of {na.a} in terms of {ganai}. By analogy with forethought version of example 12.2-5 from [CLL] p. 14.
⊢ go ko'a na.a ko'e bo'a gi ganai ko'a bo'a gi ko'e bo'a

Theorem	naai 79	Inference form of df-na.a 78 (Contributed by la korvo, 17-Aug-2023.)
⊢ ko'a na.a ko'e bo'a ⊢ ganai ko'a bo'a gi ko'e bo'a

Theorem	naaii 80	Inference form of df-na.a 78 (Contributed by la korvo, 17-Aug-2023.)
⊢ ko'a na.a ko'e bo'a ⊢ ko'a bo'a ⊢ ko'e bo'a

Theorem	naari 81	Reverse inference form of df-na.a 78 (Contributed by la korvo, 17-Aug-2023.)
⊢ ganai ko'a bo'a gi ko'e bo'a ⊢ ko'a na.a ko'e bo'a

Theorem	na.a-refl 82	{na.a} is reflexive over any brirebla. (Contributed by la korvo, 14-Aug-2024.)
⊢ ko'a na.a ko'a bo'a

1.5.2 {.anai}

Syntax	sjanai 83
sumti ko'a .anai ko'e

Definition	df-anai 84	Definition of {.anai} in terms of {ganai}. By analogy with forethought version of example 12.2-5 from [CLL] p. 14.
⊢ go ko'e .anai ko'a bo'a gi ganai ko'a bo'a gi ko'e bo'a

Theorem	anaii 85	Inference form of df-anai 84 (Contributed by la korvo, 16-Aug-2023.)
⊢ ko'e .anai ko'a bo'a ⊢ ganai ko'a bo'a gi ko'e bo'a

Theorem	anaiii 86	Inference form of df-anai 84 (Contributed by la korvo, 16-Aug-2023.)
⊢ ko'e .anai ko'a bo'a ⊢ ko'a bo'a ⊢ ko'e bo'a

Theorem	anairi 87	Reverse inference form of df-anai 84 (Contributed by la korvo, 16-Aug-2023.)
⊢ ganai ko'a bo'a gi ko'e bo'a ⊢ ko'e .anai ko'a bo'a

1.5.3 {naja}

Syntax	sbnaja 88*
selbri bu'a naja bu'e

Definition	df-naja 89*	Definition of {naja} in terms of {ganai}. By analogy with example 12.2-5 of [CLL] p. 14.
⊢ go ko'a bu'a naja bu'e ko'e gi ganai ko'a bu'a ko'e gi ko'a bu'e ko'e

Theorem	najai 90*	Inference form of df-naja 89 (Contributed by la korvo, 17-Aug-2023.)
⊢ ko'a bu'a naja bu'e ko'e ⊢ ganai ko'a bu'a ko'e gi ko'a bu'e ko'e

Theorem	najaii 91*	Inference form of df-naja 89 (Contributed by la korvo, 17-Aug-2023.)
⊢ ko'a bu'a naja bu'e ko'e ⊢ ko'a bu'a ko'e ⊢ ko'a bu'e ko'e

Theorem	najari 92*	Reverse inference form of df-naja 89 (Contributed by la korvo, 17-Aug-2023.)
⊢ ganai ko'a bu'a ko'e gi ko'a bu'e ko'e ⊢ ko'a bu'a naja bu'e ko'e

Definition	df-naja-t 93*	Extension of df-naja 89 to ternary bridi.
⊢ go ko'a bu'a naja bu'e ko'e ko'i gi ganai ko'a bu'a ko'e ko'i gi ko'a bu'e ko'e ko'i

1.5.4 {janai}

Syntax	sbjanai 94*
selbri bu'a janai bu'e

Definition	df-janai 95*	Definition of {janai} in terms of {ganai}. By analogy with example 12.2-5 of [CLL] p. 14.
⊢ go ko'a bu'e janai bu'a ko'e gi ganai ko'a bu'a ko'e gi ko'a bu'e ko'e

Theorem	janaii 96*	Inference form of df-janai 95 (Contributed by la korvo, 16-Aug-2023.)
⊢ ko'a bu'e janai bu'a ko'e ⊢ ganai ko'a bu'a ko'e gi ko'a bu'e ko'e

Theorem	janaiii 97*	Inference form of df-janai 95 (Contributed by la korvo, 16-Aug-2023.)
⊢ ko'a bu'e janai bu'a ko'e ⊢ ko'a bu'a ko'e ⊢ ko'a bu'e ko'e

Theorem	janairi 98*	Reverse inference form of df-janai 95 (Contributed by la korvo, 16-Aug-2023.)
⊢ ganai ko'a bu'a ko'e gi ko'a bu'e ko'e ⊢ ko'a bu'e janai bu'a ko'e

1.5.5 {nagi'a}

Syntax	tnagiha 99
brirebla bo'a nagi'a bo'e

Definition	df-nagiha 100	Definition of {nagi'a} in terms of {ganai}.
⊢ go ko'a bo'a nagi'a bo'e gi ganai ko'a bo'a gi ko'a bo'e

< 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-774

< Previous Next >