P. 6 of Theorem List - brismu bridi

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

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

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

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

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

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

2.16.4 {nibli}

Syntax	sbnibli 505
selbri nibli

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

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

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

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

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

2.16.5 {sigda}

Syntax	sbsigda 511
selbri sigda

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

2.16.6 {tsida}

Syntax	sbtsida 513
selbri tsida

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

2.16.7 {kanxe}

Syntax	sbkanxe 515
selbri kanxe

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

2.16.8 {vlina}

Syntax	sbvlina 517
selbri vlina

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

2.16.9 {nalti}

Syntax	sbnalti 519
selbri nalti

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

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

2.17 Parallel reasoning: {fa'u}

2.17.1 {fa'u}

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

Definition	df-fahu 523	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 524	Inference form of df-fahu 523 (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 525	Inference form of df-fahu 523 (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 526	Inference form of df-fahu 523 (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 527	Reverse inference form of df-fahu 523 (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.18 Deletion: {zi'o}

Syntax	sziho 528
sumti zi'o

Definition	df-ziho 529	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 530	Inference form of df-ziho 529 (Contributed by la korvo, 22-Aug-2024.)
⊢ ko'a bo'a ⊢ zi'o bo'a

Theorem	zihoit 531	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

Theorem	zihogi 532	First-order generalization of zihoi 530 (Contributed by la korvo, 12-Jul-2025.)
⊢ ro da zo'u da bo'a ⊢ zi'o bo'a

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

2.19.1 Transitivity: {takni}

Syntax	sbtakni 533
selbri takni

Definition	df-takni 534*	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 535*	Inference form of df-takni 534 (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.19.2 Symmetry: {kinfi}

Syntax	sbkinfi 536
selbri kinfi

Definition	df-kinfi 537*	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 538*	Reverse inference form of df-kinfi 537 (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.19.3 Reflexivity: {kinra}

Syntax	sbkinra 539
selbri kinra

Definition	df-kinra 540	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 541	Reverse inference form of df-kinra 540 (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 542	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 ⊢ pa ka ce'u bu'a ce'u kei kinra ko'e

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

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

2.19.4 Euclidean: {efklipi}, {efklizu}

Syntax	sbefklipi 545
selbri efklipi

Syntax	sbefklizu 546
selbri efklizu

Definition	df-efklipi 547*	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 548*	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 549	Every Euclidean reflexive relation is symmetric.
⊢ ganai ko'a kinra je efklipi ko'e gi ko'a kinfi ko'e

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

2.20 Existential quantifiers II: {pa da}

Syntax	bpd 551	Syntax for uniqueness quantification.
bridi pa da zo'u broda

Definition	df-pa-da 552	Definition of {pa da} in terms of {su'o da} and {du}.
⊢ go pa 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 553	Inference form of pa-da (future) (Contributed by la korvo, 20-Aug-2023.)
⊢ pa 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 554	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 ⊢ pa da zo'u da bo'a

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

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

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

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

2.20.1 Uniqueness: {pombo}

Syntax	sbpombo 559
selbri pombo

Definition	df-pombo 560	Definition of {pombo}, by analogy with df-pa-da 552. This is a slightly stronger claim than existential uniqueness; {pa da} asserts that something exists with the given property, but {pombo} goes further and witnesses the thing.
⊢ go ko'a pombo ko'e gi ro da zo'u da ckaji ko'e gi'o du ko'a

Theorem	pomboi 561	Inference form of df-pombo 560 (Contributed by la korvo, 8-Jul-2025.)
⊢ ko'a pombo ko'e ⊢ ro da zo'u da ckaji ko'e gi'o du ko'a

Theorem	pombori 562	Reverse inference form of df-pombo 560 (Contributed by la korvo, 8-Jul-2025.)
⊢ ro da zo'u da ckaji ko'e gi'o du ko'a ⊢ ko'a pombo ko'e

2.21 Abstract algebra I: magmas, semigroups, monoids

2.21.1 Magmas: {klojere}

Syntax	sbklojere 563
selbri klojere

Definition	df-klojere 564*	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 pa 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 pa di poi ke'a cmima ko'a ku'o zo'u da bu'a de di

2.21.2 Semigroups: {kloje}

Syntax	sbkloje 565
selbri kloje

Definition	df-kloje 566*	Definition of {kloje} in terms of {klojere}: a semigroup is an associative magma.
⊢ go pa ka ce'u bu'a ce'u ce'u kei kloje ko'a gi ge pa 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.21.3 Commutative operators: {cajni}

Syntax	sbcajni 567
selbri cajni

Definition	df-cajni 568*	Definition of {cajni} in terms of {klojere}.
⊢ go pa ka ce'u bu'a ce'u ce'u kei cajni ko'a gi ge pa 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 da bu'a de di gi de bu'a da di

2.21.4 Monoids: {sezni}

Syntax	sbsezni 569
selbri sezni

Definition	df-sezni 570*	Definition of {sezni} in terms of {kloje}: a monoid is a semigroup with an identity element.
⊢ go pa ka ce'u bu'a ce'u ce'u kei sezni ko'a gi ge ko'a kloje pa ka ce'u bu'a ce'u ce'u kei gi ro da poi ke'a cmima ko'a ku'o zo'u pa 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 571*	The identity element of monoids is unique. (Contributed by la korvo, 16-Oct-2024.)
⊢ pa ka ce'u bu'a ce'u ce'u kei sezni ko'a ⊢ da cmima ko'a ⊢ pa de poi ke'a cmima ko'a ku'o zo'u ge da bu'a de da gi de bu'a da da

2.21.5 Groups: {dukni}

Syntax	sbdukni 572
selbri dukni

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 598 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 573
sumti li ku'i'a

Syntax	p0 574
PA no

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

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

Syntax	mbaihei 576
PA bai'ei ku'i'a

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

Theorem	baihei-inj 578*	Inference form of ax-baihei-inj 577 (Contributed by la korvo, 30-Aug-2024.)
⊢ li bai'ei ku'i'a du li bai'ei ku'i'e ⊢ li ku'i'a du li ku'i'e

Syntax	bkaclihe 579
selbri kacli'e

Definition	df-kaclihe 580	Definition of {kacli'e} in terms of {bai'ei}.
⊢ go li ku'i'a kacli'e ko'a gi li bai'ei ku'i'a du ko'a

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

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

Syntax	p1 583
PA pa

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

Definition	df-pa 585	One is the successor of zero.
⊢ li pa du li bai'ei no

Syntax	p2 586
PA re

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

Definition	df-re 588	Two is the successor of one.
⊢ li re du li bai'ei pa

3.1.3 Natural number predicate: {kacna'u}

Syntax	bkacnahu 589
selbri kacna'u

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

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

3.1.4 Successor II

Axiom	ax-succ-succ 592	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 577
⊢ ganai ko'a .e ko'e kacli'e ko'i gi ko'a du ko'e

Theorem	succ-succi 593	Inference form of ax-succ-succ 592 (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 594*	The induction axiom for second-order arithmetic. To accomodate higher-order relations, the selbri parameter is generalized to a brirebla.
⊢ ganai ge li no 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 595*	Inference form of ax-nat-ind 594 (Contributed by la korvo, 10-Aug-2023.)
⊢ ge li no 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 596*	Inference form of ax-nat-ind 594 (Contributed by la korvo, 10-Aug-2023.)
⊢ li no 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 597*	Curried form of ax-nat-ind 594 (Contributed by la korvo, 20-Aug-2023.)
⊢ ganai li no 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 598*	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 no gi su'o de zo'u de kacli'e da

3.1.5 Addition I: {su'i}

Syntax	msuhi 599*
PA su'i ku'i'a ku'i'e

Axiom	ax-plus-zero 600	Addition with zero. A standard axiom of second-order arithmetic. Robinson's fourth axiom.
⊢ li su'i ku'i'a no du li ku'i'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-800 9 801-900 10 901-1000 11 1001-1048

< Previous Next >