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

Definition	df-poi-pa 501	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 502	Inference form of df-poi-pa 501 (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 503	Reverse inference form of df-poi-pa 501 (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 504
selbri pombo

Definition	df-pombo 505	Definition of {pombo}, by analogy with df-pa-da 497. 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 506
selbri klojere

Definition	df-klojere 507*	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 508
selbri kloje

Definition	df-kloje 509*	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 510
selbri sezni

Definition	df-sezni 511*	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 512*	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 538 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 513
sumti li ku'i'a

Syntax	p0 514
PA 0

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

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

Syntax	mbaihei 516
PA 1+ ku'i'a

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

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

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

Syntax	p1 523
PA 1

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

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

Syntax	p2 526
PA 2

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

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

3.1.3 Natural number predicate: {kacna'u}

Syntax	bkacnahu 529
selbri kacna'u

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

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

3.1.4 Successor II

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

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

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

3.1.6 Addition II: {sumji}

Syntax	bsumji 543
selbri sumji

Definition	df-sumji 544*	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 545	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 546	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 547*
PA * ku'i'a ku'i'e

Axiom	ax-mul-zero 548	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 549*	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 550
selbri pilji

Definition	df-pilji 551*	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 552	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 553	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 554
selbri kacme'a

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

Theorem	gt-zero-ref 556	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 557	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 558
selbri tenfa

3.3 Logarithms: {dugri}

Syntax	sbdugri 559
selbri dugri

Definition	df-dugri 560	{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 561	Inference form of df-dugri 560 (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 562	Inference form of df-dugri 560 (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 563	Syntax for cardinality over arbitrary sumti.
PA # ko'a

3.4.2 {kazmi}

Syntax	sbkazmi 564
selbri kazmi

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

Axiom	ax-card-fun 566	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 567	Inference form of ax-card-fun 566 (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 568	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 569
selbri pagbu

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

Theorem	pagbu-kinra 571	{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 572	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 573	Inference form of ax-pagbu-antisym 572 (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 574	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 575	Inference form of ax-pagbu-trans 574 (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 576	The universe exists.
⊢ su'o da zo'u ko'a pagbu da

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

4.1.2 {jompau}

Syntax	sbjompau 578
selbri jompau

Definition	df-jompau 579	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 580	Inference form of df-jompau 579 (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 581	Reverse inference form of df-jompau 579 (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 582
selbri kuzypau

Definition	df-kuzypau 583	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 584	Inference form of df-kuzypau 583 (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 585	Reverse inference form of df-kuzypau 583 (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 586
selbri berti

Syntax	sbsnanu 587
selbri snanu

Syntax	sbstici 588
selbri stici

Syntax	sbstuna 589
selbri stuna

Axiom	ax-berti-snanu 590	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 591	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 592
selbri crane

Syntax	sbtrixe 593
selbri trixe

Syntax	sbzunle 594
selbri zunle

Syntax	sbpritu 595
selbri pritu

Syntax	sbgapru 596
selbri gapru

Syntax	sbcnita 597
selbri cnita

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

Axiom	ax-zunle-pritu 599	Leftward and rightward are opposite.
⊢ go ko'a zunle ko'e ko'i gi ko'e pritu ko'a ko'i

Axiom	ax-gapru-cnita 600	Upward and downward are opposite.
⊢ go ko'a gapru ko'e ko'i gi ko'e cnita 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-975

< Previous Next >