P. 6 of Theorem List - brismu bridi

Home	brismu bridi Theorem List (p. 6 of 9)	< 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 Magmas: {klojere}

Syntax	sbklojere 504
selbri klojere

Definition	df-klojere 505*	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 506
selbri kloje

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

Definition	df-sezni 509*	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 510*	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 536 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 511
sumti li ku'i'a

Syntax	p0 512
PA 0

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

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

Syntax	mbaihei 514
PA 1+ ku'i'a

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

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

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

Syntax	p1 521
PA 1

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

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

Syntax	p2 524
PA 2

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

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

3.1.3 Natural number predicate: {kacna'u}

Syntax	bkacnahu 527
selbri kacna'u

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

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

3.1.4 Successor II

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

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

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

3.1.6 Addition II: {sumji}

Syntax	bsumji 541
selbri sumji

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

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

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

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

Theorem	gt-zero-ref 554	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 555	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 556
selbri tenfa

3.3 Logarithms: {dugri}

Syntax	sbdugri 557
selbri dugri

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

3.4.2 {kazmi}

Syntax	sbkazmi 562
selbri kazmi

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

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

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

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

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

4.1.2 {jompau}

Syntax	sbjompau 576
selbri jompau

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

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

Syntax	sbsnanu 585
selbri snanu

Syntax	sbstici 586
selbri stici

Syntax	sbstuna 587
selbri stuna

Axiom	ax-berti-snanu 588	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 589	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 590
selbri crane

Syntax	sbtrixe 591
selbri trixe

Syntax	sbzunle 592
selbri zunle

Syntax	sbpritu 593
selbri pritu

Syntax	sbgapru 594
selbri gapru

Syntax	sbcnita 595
selbri cnita

Axiom	ax-crane-trixe 596	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 597	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 598	Upward and downward are opposite.
⊢ go ko'a gapru ko'e ko'i gi ko'e cnita ko'a ko'i

5.3 Minkowski spacetime

5.3.1 {cabna}

Syntax	sbcabna 599
selbri cabna

Axiom	ax-cabna-sym 600	{cabna} is symmetric.
⊢ go ko'a cabna ko'e gi ko'e cabna 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-800 9 801-827

< Previous Next >