P. 6 of Theorem List - brismu bridi

Home	brismu bridi Theorem List (p. 6 of 10)	< 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

Theorem	pa-dari 501	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 502	Restriction for first-order uniqueness quantification.
bridi 1 da poi ke'a bo'a ku'o zo'u broda

Definition	df-poi-pa 503	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 504	Inference form of df-poi-pa 503 (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 505	Reverse inference form of df-poi-pa 503 (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 Uniqueness: {pombo}

Syntax	sbpombo 506
selbri pombo

Definition	df-pombo 507	Definition of {pombo}, by analogy with df-pa-da 499. This is a slightly stronger claim than existential uniqueness; {1 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 go da ckaji ko'e gi ko'a du da

2.18.2 Magmas: {klojere}

Syntax	sbklojere 508
selbri klojere

Definition	df-klojere 509*	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.3 Semigroups: {kloje}

Syntax	sbkloje 510
selbri kloje

Definition	df-kloje 511*	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.4 Monoids: {sezni}

Syntax	sbsezni 512
selbri sezni

Definition	df-sezni 513*	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 514*	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 540 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 515
sumti li ku'i'a

Syntax	p0 516
PA 0

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

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

Syntax	mbaihei 518
PA 1+ ku'i'a

Axiom	ax-baihei-inj 519*	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 520*	Inference form of ax-baihei-inj 519 (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 521
selbri kacli'e

Definition	df-kaclihe 522	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 523	Zero is not a successor. A standard axiom of second-order arithmetic.
⊢ naku ko'a kacli'e li 0

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

Syntax	p1 525
PA 1

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

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

Syntax	p2 528
PA 2

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

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

3.1.3 Natural number predicate: {kacna'u}

Syntax	bkacnahu 531
selbri kacna'u

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

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

3.1.4 Successor II

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

Theorem	succ-succi 535	Inference form of ax-succ-succ 534 (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 536*	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 537*	Inference form of ax-nat-ind 536 (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 538*	Inference form of ax-nat-ind 536 (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 539*	Curried form of ax-nat-ind 536 (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 540*	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 541*
PA + ku'i'a ku'i'e

Axiom	ax-plus-zero 542	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 543*	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 544	1 + 0 = 1 (Contributed by la korvo, 30-Aug-2024.)
⊢ li + 1 0 du li 1

3.1.6 Addition II: {sumji}

Syntax	bsumji 545
selbri sumji

Definition	df-sumji 546*	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

Theorem	sumji-no 547	Every natural number is equal to zero plus itself. (Contributed by la korvo, 30-Aug-2024.)
⊢ li ku'i'a sumji li 0 li ku'i'a

Axiom	ax-sumji-succ 548	Addition on natural numbers is well-founded and proceeds by successors. This is Robinson axiom 5.
⊢ su'o da zo'u ge ko'i sumji ko'a da gi ko'e kacli'e da ⊢ su'o da zo'u ge da sumji ko'a ko'e gi da kacli'e ko'i

3.1.7 Multiplication I: {pi'i}

Syntax	mpihi 549*
PA * ku'i'a ku'i'e

Axiom	ax-mul-zero 550	Multiplication with zero. A standard axiom of second-order arithmetic. Robinson's sixth axiom.
⊢ li * ku'i'a 0 du li 0

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

3.1.8 Multiplication II: {pilji}

Syntax	bpilji 552
selbri pilji

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

Theorem	pilji-no 554	Every natural number times zero is zero. (Contributed by la korvo, 30-Aug-2024.)
⊢ li ku'i'a pilji li 0 li 0

Axiom	ax-pilji-succ 555	Multiplication on natural numbers is well-founded. This is Robinson axiom 7.
⊢ su'o da zo'u ge ko'i pilji ko'a da gi ko'e kacli'e da ⊢ su'o da zo'u ge ko'i sumji da ko'a gi da pilji ko'a ko'e

3.1.9 Comparison I: {kacme'a}

Syntax	bkacmeha 556
selbri kacme'a

Axiom	ax-gt-zero 557	Zero is not greater than any natural number. This is Robinson axiom 8.
⊢ naku ko'a kacme'a li 0

Theorem	gt-zero-ref 558	Refutation of any natural number less than zero. (Contributed by la korvo, 21-Jun-2024.)
⊢ ko'a kacme'a li 0 ⊢ gai'o

Definition	df-kacmeha 559	Recursive definition of {kacme'a}. This is Robinson axiom 11.
⊢ go ko'a kacme'a ko'e gi su'o da poi ke'a kacli'e ko'a zo'u ga da kacme'a ko'e gi da du ko'e

3.2 Exponents I: {tenfa}

Syntax	sbtenfa 560
selbri tenfa

3.3 Logarithms: {dugri}

Syntax	sbdugri 561
selbri dugri

Definition	df-dugri 562	{dugri} is a permutation of {tenfa}.
⊢ go ko'a dugri ko'e ko'i gi ko'a te se tenfa ko'e ko'i

Theorem	dugrii 563	Inference form of df-dugri 562 (Contributed by la korvo, 9-Aug-2023.)
⊢ ko'a dugri ko'e ko'i ⊢ ko'a te se tenfa ko'e ko'i

Theorem	dugriri 564	Inference form of df-dugri 562 (Contributed by la korvo, 9-Aug-2023.)
⊢ ko'a te se tenfa ko'e ko'i ⊢ ko'a dugri ko'e ko'i

3.4 Cardinality

3.4.1 {ka'au}

Syntax	mkahau 565	Syntax for cardinality over arbitrary sumti.
PA # ko'a

3.4.2 {kazmi}

Syntax	sbkazmi 566
selbri kazmi

Definition	df-kazmi 567	Definition of {kazmi} in terms of {#}.
⊢ go ko'a kazmi ko'e gi ko'a du li # ko'e

Axiom	ax-card-fun 568	Cardinality is a function on sets. An axiom of Fregean cardinality.
⊢ ganai ko'a .e ko'e kazmi ko'i gi ko'a du ko'e

Theorem	kazmi-funii 569	Inference form of ax-card-fun 568 (Contributed by la korvo, 31-Jul-2024.)
⊢ ko'a kazmi ko'i ⊢ ko'e kazmi ko'i ⊢ ko'a du ko'e

Axiom	ax-card-ex 570	A unary relation describes the empty set when it never holds. An axiom of Fregean cardinality.
⊢ go li 0 kazmi 1 ka ce'u bo'a kei gi naku su'o da zo'u da bo'a

PART 4 MEREOLOGY Mereology is an alternative to set theory. Where set theory focuses on elementhood, using {cmima}, mereology focuses on parthood, using {pagbu}.

4.1 Parthood

4.1.1 {pagbu}

Syntax	sbpagbu 571
selbri pagbu

Axiom	ax-pagbu-refl 572	Parthood is reflexive.
⊢ ko'a pagbu ko'a

Theorem	pagbu-kinra 573	{pagbu} is reflexive over any domain. (Contributed by la korvo, 31-Aug-2024.)
⊢ 1 ka ce'u pagbu ce'u kei kinra ko'e

Axiom	ax-pagbu-antisym 574	Parthood is antisymmetric.
⊢ ganai ge ko'a pagbu ko'e gi ko'e pagbu ko'a gi ko'a du ko'e

Theorem	pagbu-antisym 575	Inference form of ax-pagbu-antisym 574 (Contributed by la korvo, 4-Sep-2023.)
⊢ ko'a pagbu ko'e ⊢ ko'e pagbu ko'a ⊢ ko'a du ko'e

Axiom	ax-pagbu-trans 576	Parthood is transitive.
⊢ ganai ge ko'a pagbu ko'e gi ko'e pagbu ko'i gi ko'a pagbu ko'i

Theorem	pagbu-trans 577	Inference form of ax-pagbu-trans 576 (Contributed by la korvo, 4-Sep-2023.)
⊢ ko'a pagbu ko'e ⊢ ko'e pagbu ko'i ⊢ ko'a pagbu ko'i

Axiom	ax-pagbu-top 578	The universe exists.
⊢ su'o da zo'u ko'a pagbu da

Axiom	ax-pagbu-bot 579	The empty part exists.
⊢ su'o da zo'u da pagbu ko'a

4.1.2 {jompau}

Syntax	sbjompau 580
selbri jompau

Definition	df-jompau 581	Definition of {jompau} in terms of {pagbu}.
⊢ go ko'a jompau ko'e gi su'o da zo'u da pagbu ko'a .e ko'e

Theorem	jompaui 582	Inference form of df-jompau 581 (Contributed by la korvo, 4-Sep-2023.)
⊢ ko'a jompau ko'e ⊢ su'o da zo'u da pagbu ko'a .e ko'e

Theorem	jompauri 583	Reverse inference form of df-jompau 581 (Contributed by la korvo, 4-Sep-2023.)
⊢ su'o da zo'u da pagbu ko'a .e ko'e ⊢ ko'a jompau ko'e

4.1.3 {kuzypau}

Syntax	sbkuzypau 584
selbri kuzypau

Definition	df-kuzypau 585	Definition of {kuzypau} in terms of {pagbu}.
⊢ go ko'a kuzypau ko'e gi su'o da zo'u ko'a .e ko'e pagbu da

Theorem	kuzypaui 586	Inference form of df-kuzypau 585 (Contributed by la korvo, 4-Sep-2023.)
⊢ ko'a kuzypau ko'e ⊢ su'o da zo'u ko'a .e ko'e pagbu da

Theorem	kuzypauri 587	Reverse inference form of df-kuzypau 585 (Contributed by la korvo, 4-Sep-2023.)
⊢ su'o da zo'u ko'a .e ko'e pagbu da ⊢ ko'a kuzypau ko'e

PART 5 SPACE & SPACETIME

5.1 Two-dimensional Euclidean space

5.1.1 Compass directions

Syntax	sbberti 588
selbri berti

Syntax	sbsnanu 589
selbri snanu

Syntax	sbstici 590
selbri stici

Syntax	sbstuna 591
selbri stuna

Axiom	ax-berti-snanu 592	Northward and southward are opposite.
⊢ go ko'a berti ko'e ko'i gi ko'e snanu ko'a ko'i

Axiom	ax-stici-stuna 593	Westward and eastward are opposite.
⊢ go ko'a stici ko'e ko'i gi ko'e stuna ko'a ko'i

5.2 Three-dimensional Euclidean space

5.2.1 Spatial directions

Syntax	sbcrane 594
selbri crane

Syntax	sbtrixe 595
selbri trixe

Syntax	sbzunle 596
selbri zunle

Syntax	sbpritu 597
selbri pritu

Syntax	sbgapru 598
selbri gapru

Syntax	sbcnita 599
selbri cnita

Axiom	ax-crane-trixe 600	Forward and backward are opposite.
⊢ go ko'a crane ko'e ko'i gi ko'e trixe ko'a ko'i

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

< Previous Next >