P. 5 of Theorem List - brismu bridi

Home	brismu bridi Theorem List (p. 5 of 8)	< Previous Next >
		Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List

**Theorem List for brismu bridi -** 401-500 *Has distinct variable group(s)
Type	Label	Description
Statement

Definition	df-bridi-q 401
⊢ 1 du'u ko'a bu'a ko'e ko'i ko'o kei bridi 1 ka ce'u bu'a ce'u ce'u ce'u kei ko'a ce'o ko'e ce'o ko'i ce'o ko'o

Syntax	sbselbri 402
selbri selbri

Definition	df-selbri 403
⊢ go ko'a selbri ko'e ko'i gi ko'a se bridi ko'e ko'i

2.14.3 {fatci}

Syntax	sbfatci 404
selbri fatci

Definition	df-fatci 405	Definition of {fatci} in terms of {du'u}.
⊢ go 1 du'u broda kei fatci gi broda

Theorem	fatcii 406	Inference form of df-fatci 405 (Contributed by la korvo, 10-Mar-2024.)
⊢ 1 du'u broda kei fatci ⊢ broda

Theorem	fatciri 407	Reverse inference form of df-fatci 405 (Contributed by la korvo, 10-Mar-2024.)
⊢ broda ⊢ 1 du'u broda kei fatci

Theorem	fatci-ceihi 408	{cei'i} is absolutely true when abstracted. (Contributed by la korvo, 10-Mar-2024.)
⊢ 1 du'u cei'i kei fatci

2.14.4 {nibli}

Syntax	sbnibli 409
selbri nibli

Definition	df-nibli 410	{nibli} internalizes implication.
⊢ go 1 du'u broda kei nibli 1 du'u brode kei gi ganai broda gi brode

Theorem	niblii 411	Inference form of df-nibli 410 (Contributed by la korvo, 19-Jul-2024.)
⊢ 1 du'u broda kei nibli 1 du'u brode kei ⊢ ganai broda gi brode

Theorem	nibliii 412	Inference form of df-nibli 410 (Contributed by la korvo, 19-Jul-2024.)
⊢ 1 du'u broda kei nibli 1 du'u brode kei ⊢ broda ⊢ brode

Theorem	nibliri 413	Reverse inference form of df-nibli 410 (Contributed by la korvo, 19-Jul-2024.)
⊢ ganai broda gi brode ⊢ 1 du'u broda kei nibli 1 du'u brode kei

Theorem	nibli-refl 414	{nibli} is reflexive. (Contributed by la korvo, 19-Jul-2024.)
⊢ 1 du'u broda kei nibli 1 du'u broda kei

2.14.5 {sigda}

Syntax	sbsigda 415
selbri sigda

Definition	df-sigda 416	{sigda} internalizes implication.
⊢ 1 du'u ganai broda gi brode kei sigda 1 du'u broda kei 1 du'u brode kei

2.14.6 {tsida}

Syntax	sbtsida 417
selbri tsida

Definition	df-tsida 418	{tsida} internalizes biimplication.
⊢ 1 du'u go broda gi brode kei tsida 1 du'u broda kei 1 du'u brode kei

2.14.7 {kanxe}

Syntax	sbkanxe 419
selbri kanxe

Definition	df-kanxe 420	{kanxe} internalizes conjunction.
⊢ 1 du'u ge broda gi brode kei kanxe 1 du'u broda kei 1 du'u brode kei

2.14.8 {vlina}

Syntax	sbvlina 421
selbri vlina

Definition	df-vlina 422	{vlina} internalizes disjunction.
⊢ 1 du'u ga broda gi brode kei vlina 1 du'u broda kei 1 du'u brode kei

2.14.9 {nalti}

Syntax	sbnalti 423
selbri nalti

Definition	df-nalti-ana 424	{nalti} internalizes negation. This direction adds the {naku zo'u} prenex to the second bridi.
⊢ 1 du'u broda kei nalti 1 du'u naku zo'u broda kei

Definition	df-nalti-kata 425	{nalti} internalizes negation. This direction adds the {naku zo'u} prenex to the first bridi.
⊢ 1 du'u naku zo'u broda kei nalti 1 du'u broda kei

2.15 Parallel reasoning: {fa'u}

2.15.1 {fa'u}

Syntax	sfahu 426
sumti ko'a fa'u ko'e

Definition	df-fahu 427	Definition of {fa'u} in terms of {ge}.
⊢ go ko'a fa'u ko'e bu'a ko'i fa'u ko'o gi ge ko'a bu'a ko'i gi ko'e bu'a ko'o

Theorem	fahui 428	Inference form of df-fahu 427 (Contributed by la korvo, 16-Jun-2024.)
⊢ ko'a fa'u ko'e bu'a ko'i fa'u ko'o ⊢ ge ko'a bu'a ko'i gi ko'e bu'a ko'o

Theorem	fahuil 429	Inference form of df-fahu 427 (Contributed by la korvo, 16-Jun-2024.)
⊢ ko'a fa'u ko'e bu'a ko'i fa'u ko'o ⊢ ko'a bu'a ko'i

Theorem	fahuir 430	Inference form of df-fahu 427 (Contributed by la korvo, 16-Jun-2024.)
⊢ ko'a fa'u ko'e bu'a ko'i fa'u ko'o ⊢ ko'e bu'a ko'o

Theorem	fahuri 431	Reverse inference form of df-fahu 427 (Contributed by la korvo, 16-Jun-2024.)
⊢ ko'a bu'a ko'i ⊢ ko'e bu'a ko'o ⊢ ko'a fa'u ko'e bu'a ko'i fa'u ko'o

2.16 Deletion: {zi'o}

Syntax	sziho 432
sumti zi'o

Definition	df-ziho 433	Definition of {zi'o}. Justified by example 7.4-7 from [CLL] p. 7.
⊢ ganai ko'a bo'a gi zi'o bo'a

Theorem	zihoi 434	Inference form of df-ziho 433 (Contributed by la korvo, 22-Aug-2024.)
⊢ ko'a bo'a ⊢ zi'o bo'a

Theorem	zihoit 435	Delete the second place of a binary bridi. (Contributed by la korvo, 22-Aug-2024.)
⊢ ko'a bu'a ko'e ⊢ ko'a bu'a zi'o

2.17 Properties of relations We investigate several common non-familial properties of relations.

2.17.1 Transitivity: {takni}

Syntax	sbtakni 436
selbri takni

Definition	df-takni 437*	A standard definition of transitive relations.
⊢ go ko'a takni ko'e gi ro da poi ke'a cmima ko'e ku'o zo'u ro de poi ke'a cmima ko'e ku'o zo'u ro di poi ke'a cmima ko'e ku'o zo'u ganai ge da ckini de ko'a gi de ckini di ko'a gi da ckini di ko'a

Theorem	taknii 438*	Inference form of df-takni 437 (Contributed by la korvo, 22-Jun-2024.)
⊢ ko'a takni ko'e ⊢ ro da poi ke'a cmima ko'e ku'o zo'u ro de poi ke'a cmima ko'e ku'o zo'u ro di poi ke'a cmima ko'e ku'o zo'u ganai ge da ckini de ko'a gi de ckini di ko'a gi da ckini di ko'a

2.17.2 Symmetry: {kinfi}

Syntax	sbkinfi 439
selbri kinfi

Definition	df-kinfi 440*	A standard definition of symmetric relations.
⊢ go ko'a kinfi ko'e gi ro da poi ke'a cmima ko'e ku'o zo'u ro de poi ke'a cmima ko'e ku'o zo'u ganai da ckini de ko'a gi de ckini da ko'a

Theorem	kinfiri 441*	Reverse inference form of df-kinfi 440 (Contributed by la korvo, 25-Jun-2024.)
⊢ ro da poi ke'a cmima ko'e ku'o zo'u ro de poi ke'a cmima ko'e ku'o zo'u ganai da ckini de ko'a gi de ckini da ko'a ⊢ ko'a kinfi ko'e

2.17.3 Reflexivity: {kinra}

Syntax	sbkinra 442
selbri kinra

Definition	df-kinra 443	A standard definition of reflexive relations.
⊢ go ko'a kinra ko'e gi ro da poi ke'a cmima ko'e ku'o zo'u da ckini da ko'a

Theorem	kinrari 444	Reverse inference form of df-kinra 443 (Contributed by la korvo, 25-Jun-2024.)
⊢ ro da poi ke'a cmima ko'e ku'o zo'u da ckini da ko'a ⊢ ko'a kinra ko'e

Theorem	refl-kinra 445	If a selbri is reflexive over any metasyntactic terbri, then it is reflexive over any domain. (Contributed by la korvo, 13-Aug-2024.)
⊢ da bu'a da ⊢ 1 ka ce'u bu'a ce'u kei kinra ko'e

Theorem	du-kinra 446	{du} is reflexive over any domain. (Contributed by la korvo, 25-Jun-2024.)
⊢ 1 ka ce'u du ce'u kei kinra ko'e

Theorem	gripau-kinra 447	{gripau} is reflexive over any domain. (Contributed by la korvo, 19-Jul-2024.)
⊢ 1 ka ce'u gripau ce'u kei kinra ko'e

2.17.4 Euclidean: {efklipi}, {efklizu}

Syntax	sbefklipi 448
selbri efklipi

Syntax	sbefklizu 449
selbri efklizu

Definition	df-efklipi 450*	A standard definition of right-Euclidean relations.
⊢ go ko'a efklipi ko'e gi ro da poi ke'a cmima ko'e ku'o zo'u ro de poi ke'a cmima ko'e ku'o zo'u ro di poi ke'a cmima ko'e ku'o zo'u ganai da ckini de .e di ko'a gi de ckini di ko'a

Definition	df-efklizu 451*	A standard definition of left-Euclidean relations.
⊢ go ko'a efklizu ko'e gi ro da poi ke'a cmima ko'e ku'o zo'u ro de poi ke'a cmima ko'e ku'o zo'u ro di poi ke'a cmima ko'e ku'o zo'u ganai de .e di ckini da ko'a gi de ckini di ko'a

Axiom	ax-efklipi-sym 452	Every Euclidean reflexive relation is symmetric.
⊢ ganai ko'a kinra je efklipi ko'e gi ko'a kinfi ko'e

Axiom	ax-efklizu-sym 453
⊢ ganai ko'a kinra je efklizu ko'e gi ko'a kinfi ko'e

2.18 Existential quantifiers II: {pa da}

Syntax	bpd 454	Syntax for uniqueness quantification.
bridi 1 da zo'u broda

Definition	df-pa-da 455	Definition of {1 da} in terms of {su'o da} and {du}.
⊢ go 1 da zo'u da bo'a gi su'o da zo'u ge da bo'a gi ganai ko'a bo'a gi ko'a du da

Theorem	pa-dai 456	Inference form of pa-da (future) (Contributed by la korvo, 20-Aug-2023.)
⊢ 1 da zo'u da bo'a ⊢ su'o da zo'u ge da bo'a gi ganai ko'a bo'a gi ko'a du da

Theorem	pa-dari 457	Reverse inference form of pa-da (future) (Contributed by la korvo, 20-Aug-2023.)
⊢ su'o da zo'u ge da bo'a gi ganai ko'a bo'a gi ko'a du da ⊢ 1 da zo'u da bo'a

Syntax	bpdp 458	Restriction for first-order uniqueness quantification.
bridi 1 da zo'u broda bridi 1 da poi ke'a bo'a ku'o zo'u broda

Definition	df-poi-pa 459	Definition of {1 da poi} quantifiers as restricted first-order uniqueness quantifiers.
⊢ go 1 da poi ke'a bo'a ku'o zo'u broda gi 1 da zo'u ganai da bo'a gi broda

Theorem	poi-pai 460	Inference form of df-poi-pa 459 (Contributed by la korvo, 15-Oct-2024.)
⊢ 1 da poi ke'a bo'a ku'o zo'u broda ⊢ 1 da zo'u ganai da bo'a gi broda

Theorem	poi-pari 461	Reverse inference form of df-poi-pa 459 (Contributed by la korvo, 15-Oct-2024.)
⊢ 1 da zo'u ganai da bo'a gi broda ⊢ 1 da poi ke'a bo'a ku'o zo'u broda

2.18.1 Magmas: {klojere}

Syntax	sbklojere 462
selbri klojere

Definition	df-klojere 463*	Definition of {klojere}. This is our most foundational definition for binary operators for now: a binary operator is a ternary relation closed over a set such that, for every ordered pair of elements in the closure, there is a unique related element. In terms of abstract algebra, our binary operators are magmas.
⊢ go 1 ka ce'u bu'a ce'u ce'u kei klojere ko'a gi ro da poi ke'a cmima ko'a ku'o zo'u ro de poi ke'a cmima ko'a ku'o zo'u 1 di poi ke'a cmima ko'a ku'o zo'u da bu'a de di

2.18.2 Semigroups: {kloje}

Syntax	sbkloje 464
selbri kloje

Definition	df-kloje 465*	Definition of {kloje} in terms of {klojere}: a semigroup is an associative magma.
⊢ go 1 ka ce'u bu'a ce'u ce'u kei kloje ko'a gi ge 1 ka ce'u bu'a ce'u ce'u kei klojere ko'a gi ro da poi ke'a cmima ko'a ku'o zo'u ro de poi ke'a cmima ko'a ku'o zo'u ro di poi ke'a cmima ko'a ku'o zo'u go ge da bu'a de ko'e gi ko'e bu'a di ko'i gi ge de bu'a di ko'e gi di bu'a ko'e ko'i

2.18.3 Monoids: {sezni}

Syntax	sbsezni 466
selbri sezni

Definition	df-sezni 467*	Definition of {sezni} in terms of {kloje}: a monoid is a semigroup with an identity element.
⊢ go 1 ka ce'u bu'a ce'u ce'u kei sezni ko'a gi ge ko'a kloje 1 ka ce'u bu'a ce'u ce'u kei gi ro da poi ke'a cmima ko'a ku'o zo'u 1 de poi ke'a cmima ko'a ku'o zo'u ge da bu'a de da gi de bu'a da da

Theorem	sezni-elt 468*	The identity element of monoids is unique. (Contributed by la korvo, 16-Oct-2024.)
⊢ 1 ka ce'u bu'a ce'u ce'u kei sezni ko'a ⊢ da cmima ko'a ⊢ 1 de poi ke'a cmima ko'a ku'o zo'u ge da bu'a de da gi de bu'a da da

PART 3 NUMBERS We define the standard gadgets of number theory. Our axioms are based on the Robinson axioms for second-order arithmetic over successor, addition, multiplication, and comparison. We apply the standard intuitionistic and Metamath transformations to these axioms in addition to reframing them for a Lojbanic relation-first presentation. Further directions include proving ax-succ-std 494 by improving the axiom of induction, as well as introducing and proving the other Robinson axioms using induction. At the moment, induction can only handle closed formulae expressible as brirebla ({da bo'a}), which proves to be an obstacle.

3.1 Natural numbers We build the natural numbers first with {li} and {du} to match standard presentations, then again with {kacna'u} to establish properties of the set of natural numbers.

3.1.1 Zero: {li no}

Syntax	sli 469
sumti li ku'i'a

Syntax	p0 470
PA 0

Theorem	sl0 471	Syntax for zero. (Contributed by la korvo, 31-Jul-2024.)
sumti li 0

3.1.2 Successor I: {bai'ei}, {kacli'e}

Syntax	mbaihei 472
PA 1+ ku'i'a

Axiom	ax-baihei-inj 473*	The successor function is injective. A standard axiom of second-order arithmetic.
⊢ ganai li 1+ ku'i'a du li 1+ ku'i'e gi li ku'i'a du li ku'i'e

Theorem	baihei-inj 474*	Inference form of ax-baihei-inj 473 (Contributed by la korvo, 30-Aug-2024.)
⊢ li 1+ ku'i'a du li 1+ ku'i'e ⊢ li ku'i'a du li ku'i'e

Syntax	bkaclihe 475
selbri kacli'e

Definition	df-kaclihe 476	Definition of {kacli'e} in terms of {1+}.
⊢ go li ku'i'a kacli'e ko'a gi li 1+ ku'i'a du ko'a

Axiom	ax-succ-zero 477	Zero is not a successor. A standard axiom of second-order arithmetic.
⊢ naku zo'u ko'a kacli'e li 0

Theorem	succ-zero-ref 478	Refutation of any claimed predecessor to zero. (Contributed by la korvo, 20-Aug-2023.)
⊢ ko'a kacli'e li 0 ⊢ gai'o

Syntax	p1 479
PA 1

Theorem	sl1 480	Syntax for one. (Contributed by la korvo, 31-Jul-2024.)
sumti li 1

Definition	df-pa 481	One is the successor of zero.
⊢ li 1 du li 1+ 0

Syntax	p2 482
PA 2

Theorem	sl2 483	Syntax for two. (Contributed by la korvo, 31-Jul-2024.)
sumti li 2

Definition	df-re 484	Two is the successor of one.
⊢ li 2 du li 1+ 1

3.1.3 Natural number predicate: {kacna'u}

Syntax	bkacnahu 485
selbri kacna'u

Axiom	ax-nat-no 486	Zero is a natural number. A standard axiom of second-order arithmetic.
⊢ li 0 kacna'u

Axiom	ax-nat-pa 487	One is a natural number.
⊢ li 1 kacna'u

3.1.4 Successor II

Axiom	ax-succ-succ 488	Successors of natural numbers are also natural numbers, and each natural number has exactly one successor. This is equivalent to Robinson axiom 2 and, as such, should be provable from ax-baihei-inj 473
⊢ ganai ko'a .e ko'e kacli'e ko'i gi ko'a du ko'e

Theorem	succ-succi 489	Inference form of ax-succ-succ 488 (Contributed by la korvo, 7-Jul-2024.)
⊢ ko'a .e ko'e kacli'e ko'i ⊢ ko'a du ko'e

Axiom	ax-nat-ind 490*	The induction axiom for second-order arithmetic. To accomodate higher-order relations, the selbri parameter is generalized to a brirebla.
⊢ ganai ge li 0 bo'a gi ro da poi ke'a bo'a ku'o zo'u su'o de zo'u ge da kacli'e de gi de bo'a gi ro da poi ke'a kacna'u ku'o zo'u da bo'a

Theorem	nat-indi 491*	Inference form of ax-nat-ind 490 (Contributed by la korvo, 10-Aug-2023.)
⊢ ge li 0 bo'a gi ro da poi ke'a bo'a ku'o zo'u su'o de zo'u ge da kacli'e de gi de bo'a ⊢ ro da poi ke'a kacna'u ku'o zo'u da bo'a

Theorem	nat-indii 492*	Inference form of ax-nat-ind 490 (Contributed by la korvo, 10-Aug-2023.)
⊢ li 0 bo'a ⊢ ro da poi ke'a bo'a ku'o zo'u su'o de zo'u ge da kacli'e de gi de bo'a ⊢ ro da poi ke'a kacna'u ku'o zo'u da bo'a

Theorem	nat-ind-cur 493*	Curried form of ax-nat-ind 490 (Contributed by la korvo, 20-Aug-2023.)
⊢ ganai li 0 bo'a gi ganai ro da poi ke'a bo'a ku'o zo'u su'o de zo'u ge da kacli'e de gi de bo'a gi ro da poi ke'a kacna'u ku'o zo'u da bo'a

Axiom	ax-succ-std 494*	There are no non-standard natural numbers. This axiom upgrades our arithmetic from BA, "baby arithmetic", to Robinson's Q. This is Robinson axiom 3.
⊢ ro da poi ke'a kacna'u ku'o zo'u ga da du li 0 gi su'o de zo'u de kacli'e da

3.1.5 Addition I: {su'i}

Syntax	msuhi 495*
PA + ku'i'a ku'i'e

Axiom	ax-plus-zero 496	Addition with zero. A standard axiom of second-order arithmetic. Robinson's fourth axiom.
⊢ li + ku'i'a 0 du li ku'i'a

Axiom	ax-plus-succ 497*	Addition with successor. A standard axiom of second-order arithmetic.
⊢ li + ku'i'a 1+ ku'i'e du li 1+ + ku'i'a ku'i'e

Theorem	1p0e1 498	1 + 0 = 1 (Contributed by la korvo, 30-Aug-2024.)
⊢ li + 1 0 du li 1

3.1.6 Addition II: {sumji}

Syntax	bsumji 499
selbri sumji

Definition	df-sumji 500*	Definition of {sumji} in terms of {+}.
⊢ go li ku'i'a sumji li ku'i'e ko'a gi li + ku'i'a ku'i'e du ko'a

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