![]() |
Metamath
Proof Explorer Theorem List (p. 347 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cvmlift2lem10 34601* | Lemma for cvmlift2 34605. (Contributed by Mario Carneiro, 1-Jun-2015.) |
β’ π΅ = βͺ πΆ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β ((II Γt II) Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (0πΊ0)) & β’ π» = (β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π§πΊ0)) β§ (πβ0) = π)) & β’ πΎ = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ ((β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π₯πΊπ§)) β§ (πβ0) = (π»βπ₯)))βπ¦)) & β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ β π (βπ β (π β {π})(π β© π) = β β§ (πΉ βΎ π) β ((πΆ βΎt π)Homeo(π½ βΎt π))))}) & β’ (π β π β (0[,]1)) & β’ (π β π β (0[,]1)) β β’ (π β βπ’ β II βπ£ β II (π β π’ β§ π β π£ β§ (βπ€ β π£ (πΎ βΎ (π’ Γ {π€})) β (((II Γt II) βΎt (π’ Γ {π€})) Cn πΆ) β (πΎ βΎ (π’ Γ π£)) β (((II Γt II) βΎt (π’ Γ π£)) Cn πΆ)))) | ||
Theorem | cvmlift2lem11 34602* | Lemma for cvmlift2 34605. (Contributed by Mario Carneiro, 1-Jun-2015.) |
β’ π΅ = βͺ πΆ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β ((II Γt II) Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (0πΊ0)) & β’ π» = (β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π§πΊ0)) β§ (πβ0) = π)) & β’ πΎ = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ ((β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π₯πΊπ§)) β§ (πβ0) = (π»βπ₯)))βπ¦)) & β’ π = {π§ β ((0[,]1) Γ (0[,]1)) β£ πΎ β (((II Γt II) CnP πΆ)βπ§)} & β’ (π β π β II) & β’ (π β π β II) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (βπ€ β π (πΎ βΎ (π Γ {π€})) β (((II Γt II) βΎt (π Γ {π€})) Cn πΆ) β (πΎ βΎ (π Γ π)) β (((II Γt II) βΎt (π Γ π)) Cn πΆ))) β β’ (π β ((π Γ {π}) β π β (π Γ {π}) β π)) | ||
Theorem | cvmlift2lem12 34603* | Lemma for cvmlift2 34605. (Contributed by Mario Carneiro, 1-Jun-2015.) |
β’ π΅ = βͺ πΆ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β ((II Γt II) Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (0πΊ0)) & β’ π» = (β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π§πΊ0)) β§ (πβ0) = π)) & β’ πΎ = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ ((β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π₯πΊπ§)) β§ (πβ0) = (π»βπ₯)))βπ¦)) & β’ π = {π§ β ((0[,]1) Γ (0[,]1)) β£ πΎ β (((II Γt II) CnP πΆ)βπ§)} & β’ π΄ = {π β (0[,]1) β£ ((0[,]1) Γ {π}) β π} & β’ π = {β¨π, π‘β© β£ (π‘ β (0[,]1) β§ βπ’ β ((neiβII)β{π})((π’ Γ {π}) β π β (π’ Γ {π‘}) β π))} β β’ (π β πΎ β ((II Γt II) Cn πΆ)) | ||
Theorem | cvmlift2lem13 34604* | Lemma for cvmlift2 34605. (Contributed by Mario Carneiro, 7-May-2015.) |
β’ π΅ = βͺ πΆ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β ((II Γt II) Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (0πΊ0)) & β’ π» = (β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π§πΊ0)) β§ (πβ0) = π)) & β’ πΎ = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ ((β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π₯πΊπ§)) β§ (πβ0) = (π»βπ₯)))βπ¦)) β β’ (π β β!π β ((II Γt II) Cn πΆ)((πΉ β π) = πΊ β§ (0π0) = π)) | ||
Theorem | cvmlift2 34605* | A two-dimensional version of cvmlift 34588. There is a unique lift of functions on the unit square II Γt II which commutes with the covering map. (Contributed by Mario Carneiro, 1-Jun-2015.) |
β’ π΅ = βͺ πΆ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β ((II Γt II) Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (0πΊ0)) β β’ (π β β!π β ((II Γt II) Cn πΆ)((πΉ β π) = πΊ β§ (0π0) = π)) | ||
Theorem | cvmliftphtlem 34606* | Lemma for cvmliftpht 34607. (Contributed by Mario Carneiro, 6-Jul-2015.) |
β’ π΅ = βͺ πΆ & β’ π = (β©π β (II Cn πΆ)((πΉ β π) = πΊ β§ (πβ0) = π)) & β’ π = (β©π β (II Cn πΆ)((πΉ β π) = π» β§ (πβ0) = π)) & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβ0)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π» β (II Cn π½)) & β’ (π β πΎ β (πΊ(PHtpyβπ½)π»)) & β’ (π β π΄ β ((II Γt II) Cn πΆ)) & β’ (π β (πΉ β π΄) = πΎ) & β’ (π β (0π΄0) = π) β β’ (π β π΄ β (π(PHtpyβπΆ)π)) | ||
Theorem | cvmliftpht 34607* | If πΊ and π» are path-homotopic, then their lifts π and π are also path-homotopic. (Contributed by Mario Carneiro, 6-Jul-2015.) |
β’ π΅ = βͺ πΆ & β’ π = (β©π β (II Cn πΆ)((πΉ β π) = πΊ β§ (πβ0) = π)) & β’ π = (β©π β (II Cn πΆ)((πΉ β π) = π» β§ (πβ0) = π)) & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβ0)) & β’ (π β πΊ( βphβπ½)π») β β’ (π β π( βphβπΆ)π) | ||
Theorem | cvmlift3lem1 34608* | Lemma for cvmlift3 34617. (Contributed by Mario Carneiro, 6-Jul-2015.) |
β’ π΅ = βͺ πΆ & β’ π = βͺ πΎ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΎ β SConn) & β’ (π β πΎ β π-Locally PConn) & β’ (π β π β π) & β’ (π β πΊ β (πΎ Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβπ)) & β’ (π β π β (II Cn πΎ)) & β’ (π β (πβ0) = π) & β’ (π β π β (II Cn πΎ)) & β’ (π β (πβ0) = π) & β’ (π β (πβ1) = (πβ1)) β β’ (π β ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π))β1) = ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π))β1)) | ||
Theorem | cvmlift3lem2 34609* | Lemma for cvmlift2 34605. (Contributed by Mario Carneiro, 6-Jul-2015.) |
β’ π΅ = βͺ πΆ & β’ π = βͺ πΎ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΎ β SConn) & β’ (π β πΎ β π-Locally PConn) & β’ (π β π β π) & β’ (π β πΊ β (πΎ Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβπ)) β β’ ((π β§ π β π) β β!π§ β π΅ βπ β (II Cn πΎ)((πβ0) = π β§ (πβ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π))β1) = π§)) | ||
Theorem | cvmlift3lem3 34610* | Lemma for cvmlift2 34605. (Contributed by Mario Carneiro, 6-Jul-2015.) |
β’ π΅ = βͺ πΆ & β’ π = βͺ πΎ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΎ β SConn) & β’ (π β πΎ β π-Locally PConn) & β’ (π β π β π) & β’ (π β πΊ β (πΎ Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβπ)) & β’ π» = (π₯ β π β¦ (β©π§ β π΅ βπ β (II Cn πΎ)((πβ0) = π β§ (πβ1) = π₯ β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π))β1) = π§))) β β’ (π β π»:πβΆπ΅) | ||
Theorem | cvmlift3lem4 34611* | Lemma for cvmlift2 34605. (Contributed by Mario Carneiro, 6-Jul-2015.) |
β’ π΅ = βͺ πΆ & β’ π = βͺ πΎ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΎ β SConn) & β’ (π β πΎ β π-Locally PConn) & β’ (π β π β π) & β’ (π β πΊ β (πΎ Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβπ)) & β’ π» = (π₯ β π β¦ (β©π§ β π΅ βπ β (II Cn πΎ)((πβ0) = π β§ (πβ1) = π₯ β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π))β1) = π§))) β β’ ((π β§ π β π) β ((π»βπ) = π΄ β βπ β (II Cn πΎ)((πβ0) = π β§ (πβ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π))β1) = π΄))) | ||
Theorem | cvmlift3lem5 34612* | Lemma for cvmlift2 34605. (Contributed by Mario Carneiro, 6-Jul-2015.) |
β’ π΅ = βͺ πΆ & β’ π = βͺ πΎ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΎ β SConn) & β’ (π β πΎ β π-Locally PConn) & β’ (π β π β π) & β’ (π β πΊ β (πΎ Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβπ)) & β’ π» = (π₯ β π β¦ (β©π§ β π΅ βπ β (II Cn πΎ)((πβ0) = π β§ (πβ1) = π₯ β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π))β1) = π§))) β β’ (π β (πΉ β π») = πΊ) | ||
Theorem | cvmlift3lem6 34613* | Lemma for cvmlift3 34617. (Contributed by Mario Carneiro, 9-Jul-2015.) |
β’ π΅ = βͺ πΆ & β’ π = βͺ πΎ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΎ β SConn) & β’ (π β πΎ β π-Locally PConn) & β’ (π β π β π) & β’ (π β πΊ β (πΎ Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβπ)) & β’ π» = (π₯ β π β¦ (β©π§ β π΅ βπ β (II Cn πΎ)((πβ0) = π β§ (πβ1) = π₯ β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π))β1) = π§))) & β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ β π (βπ β (π β {π})(π β© π) = β β§ (πΉ βΎ π) β ((πΆ βΎt π)Homeo(π½ βΎt π))))}) & β’ (π β (πΊβπ) β π΄) & β’ (π β π β (πβπ΄)) & β’ (π β π β (β‘πΊ β π΄)) & β’ π = (β©π β π (π»βπ) β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (II Cn πΎ)) & β’ π = (β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π)) & β’ (π β ((πβ0) = π β§ (πβ1) = π β§ (π β1) = (π»βπ))) & β’ (π β π β (II Cn (πΎ βΎt π))) & β’ (π β ((πβ0) = π β§ (πβ1) = π)) & β’ πΌ = (β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = (π»βπ))) β β’ (π β (π»βπ) β π) | ||
Theorem | cvmlift3lem7 34614* | Lemma for cvmlift3 34617. (Contributed by Mario Carneiro, 9-Jul-2015.) |
β’ π΅ = βͺ πΆ & β’ π = βͺ πΎ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΎ β SConn) & β’ (π β πΎ β π-Locally PConn) & β’ (π β π β π) & β’ (π β πΊ β (πΎ Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβπ)) & β’ π» = (π₯ β π β¦ (β©π§ β π΅ βπ β (II Cn πΎ)((πβ0) = π β§ (πβ1) = π₯ β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π))β1) = π§))) & β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ β π (βπ β (π β {π})(π β© π) = β β§ (πΉ βΎ π) β ((πΆ βΎt π)Homeo(π½ βΎt π))))}) & β’ (π β (πΊβπ) β π΄) & β’ (π β π β (πβπ΄)) & β’ (π β π β (β‘πΊ β π΄)) & β’ π = (β©π β π (π»βπ) β π) & β’ (π β (πΎ βΎt π) β PConn) & β’ (π β π β πΎ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π» β ((πΎ CnP πΆ)βπ)) | ||
Theorem | cvmlift3lem8 34615* | Lemma for cvmlift2 34605. (Contributed by Mario Carneiro, 6-Jul-2015.) |
β’ π΅ = βͺ πΆ & β’ π = βͺ πΎ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΎ β SConn) & β’ (π β πΎ β π-Locally PConn) & β’ (π β π β π) & β’ (π β πΊ β (πΎ Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβπ)) & β’ π» = (π₯ β π β¦ (β©π§ β π΅ βπ β (II Cn πΎ)((πβ0) = π β§ (πβ1) = π₯ β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π))β1) = π§))) & β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ β π (βπ β (π β {π})(π β© π) = β β§ (πΉ βΎ π) β ((πΆ βΎt π)Homeo(π½ βΎt π))))}) β β’ (π β π» β (πΎ Cn πΆ)) | ||
Theorem | cvmlift3lem9 34616* | Lemma for cvmlift2 34605. (Contributed by Mario Carneiro, 7-May-2015.) |
β’ π΅ = βͺ πΆ & β’ π = βͺ πΎ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΎ β SConn) & β’ (π β πΎ β π-Locally PConn) & β’ (π β π β π) & β’ (π β πΊ β (πΎ Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβπ)) & β’ π» = (π₯ β π β¦ (β©π§ β π΅ βπ β (II Cn πΎ)((πβ0) = π β§ (πβ1) = π₯ β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π))β1) = π§))) & β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ β π (βπ β (π β {π})(π β© π) = β β§ (πΉ βΎ π) β ((πΆ βΎt π)Homeo(π½ βΎt π))))}) β β’ (π β βπ β (πΎ Cn πΆ)((πΉ β π) = πΊ β§ (πβπ) = π)) | ||
Theorem | cvmlift3 34617* | A general version of cvmlift 34588. If πΎ is simply connected and weakly locally path-connected, then there is a unique lift of functions on πΎ which commutes with the covering map. (Contributed by Mario Carneiro, 9-Jul-2015.) |
β’ π΅ = βͺ πΆ & β’ π = βͺ πΎ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΎ β SConn) & β’ (π β πΎ β π-Locally PConn) & β’ (π β π β π) & β’ (π β πΊ β (πΎ Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβπ)) β β’ (π β β!π β (πΎ Cn πΆ)((πΉ β π) = πΊ β§ (πβπ) = π)) | ||
Theorem | snmlff 34618* | The function πΉ from snmlval 34620 is a mapping from positive integers to real numbers in the range [0, 1]. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ πΉ = (π β β β¦ ((β―β{π β (1...π) β£ (ββ((π΄ Β· (π βπ)) mod π )) = π΅}) / π)) β β’ πΉ:ββΆ(0[,]1) | ||
Theorem | snmlfval 34619* | The function πΉ from snmlval 34620 maps π to the relative density of π΅ in the first π digits of the digit string of π΄ in base π . (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ πΉ = (π β β β¦ ((β―β{π β (1...π) β£ (ββ((π΄ Β· (π βπ)) mod π )) = π΅}) / π)) β β’ (π β β β (πΉβπ) = ((β―β{π β (1...π) β£ (ββ((π΄ Β· (π βπ)) mod π )) = π΅}) / π)) | ||
Theorem | snmlval 34620* | The property "π΄ is simply normal in base π ". A number is simply normal if each digit 0 β€ π < π occurs in the base- π digit string of π΄ with frequency 1 / π (which is consistent with the expectation in an infinite random string of numbers selected from 0...π β 1). (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (π β (β€β₯β2) β¦ {π₯ β β β£ βπ β (0...(π β 1))(π β β β¦ ((β―β{π β (1...π) β£ (ββ((π₯ Β· (πβπ)) mod π)) = π}) / π)) β (1 / π)}) β β’ (π΄ β (πβπ ) β (π β (β€β₯β2) β§ π΄ β β β§ βπ β (0...(π β 1))(π β β β¦ ((β―β{π β (1...π) β£ (ββ((π΄ Β· (π βπ)) mod π )) = π}) / π)) β (1 / π ))) | ||
Theorem | snmlflim 34621* | If π΄ is simply normal, then the function πΉ of relative density of π΅ in the digit string converges to 1 / π , i.e. the set of occurrences of π΅ in the digit string has natural density 1 / π . (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (π β (β€β₯β2) β¦ {π₯ β β β£ βπ β (0...(π β 1))(π β β β¦ ((β―β{π β (1...π) β£ (ββ((π₯ Β· (πβπ)) mod π)) = π}) / π)) β (1 / π)}) & β’ πΉ = (π β β β¦ ((β―β{π β (1...π) β£ (ββ((π΄ Β· (π βπ)) mod π )) = π΅}) / π)) β β’ ((π΄ β (πβπ ) β§ π΅ β (0...(π β 1))) β πΉ β (1 / π )) | ||
Syntax | cgoe 34622 | The Godel-set of membership. |
class βπ | ||
Syntax | cgna 34623 | The Godel-set for the Sheffer stroke. |
class βΌπ | ||
Syntax | cgol 34624 | The Godel-set of universal quantification. (Note that this is not a wff.) |
class βπππ | ||
Syntax | csat 34625 | The satisfaction function. |
class Sat | ||
Syntax | cfmla 34626 | The formula set predicate. |
class Fmla | ||
Syntax | csate 34627 | The β-satisfaction function. |
class Satβ | ||
Syntax | cprv 34628 | The "proves" relation. |
class β§ | ||
Definition | df-goel 34629 | Define the Godel-set of membership. Here the arguments π₯ = β¨π, πβ© correspond to vN and vP , so (β βπ1o) actually means v0 β v1 , not 0 β 1. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ βπ = (π₯ β (Ο Γ Ο) β¦ β¨β , π₯β©) | ||
Definition | df-gona 34630 | Define the Godel-set for the Sheffer stroke NAND. Here the arguments π₯ = β¨π, πβ© are also Godel-sets corresponding to smaller formulas. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ βΌπ = (π₯ β (V Γ V) β¦ β¨1o, π₯β©) | ||
Definition | df-goal 34631 | Define the Godel-set of universal quantification. Here π β Ο corresponds to vN , and π represents another formula, and this expression is [βπ₯π] = βπππ where π₯ is the π-th variable, π = [π] is the code for π. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ βπππ = β¨2o, β¨π, πβ©β© | ||
Definition | df-sat 34632* |
Define the satisfaction predicate. This recursive construction builds up
a function over wff codes (see satff 34699) and simultaneously defines the
set of assignments to all variables from π that makes the coded wff
true in the model π, where β is interpreted as the binary
relation πΈ on π.
The interpretation of the statement π β (((π Sat πΈ)βπ)βπ) is that for the model β¨π, πΈβ©, π:ΟβΆπ is a
valuation of the variables (v0 = (πββ
), v1 = (πβ1o), etc.) and π is a code for a wff using β , βΌ , β that
is true under the assignment π. The function is defined by finite
recursion; ((π Sat πΈ)βπ) only operates on wffs of depth at
most π β Ο, and ((π Sat πΈ)βΟ) = βͺ π β Ο((π Sat πΈ)βπ) operates on all wffs.
The coding scheme for the wffs is defined so that
(Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ Sat = (π β V, π β V β¦ (rec((π β V β¦ (π βͺ {β¨π₯, π¦β© β£ βπ’ β π (βπ£ β π (π₯ = ((1st βπ’)βΌπ(1st βπ£)) β§ π¦ = ((π βm Ο) β ((2nd βπ’) β© (2nd βπ£)))) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = {π β (π βm Ο) β£ βπ§ β π ({β¨π, π§β©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)}))})), {β¨π₯, π¦β© β£ βπ β Ο βπ β Ο (π₯ = (πβππ) β§ π¦ = {π β (π βm Ο) β£ (πβπ)π(πβπ)})}) βΎ suc Ο)) | ||
Definition | df-sate 34633* | A simplified version of the satisfaction predicate, using the standard membership relation and eliminating the extra variable π. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ Satβ = (π β V, π’ β V β¦ (((π Sat ( E β© (π Γ π)))βΟ)βπ’)) | ||
Definition | df-fmla 34634 | Define the predicate which defines the set of valid Godel formulas. The parameter π defines the maximum height of the formulas: the set (Fmlaββ ) is all formulas of the form π₯ β π¦ (which in our coding scheme is the set ({β } Γ (Ο Γ Ο)); see df-sat 34632 for the full coding scheme), see fmla0 34671, and each extra level adds to the complexity of the formulas in (Fmlaβπ), see fmlasuc 34675. Remark: it is sufficient to have atomic formulas of the form π₯ β π¦ only, because equations (formulas of the form π₯ = π¦), which are required as (atomic) formulas, can be introduced as a defined notion in terms of βπ, see df-goeq 34733. (FmlaβΟ) = βͺ π β Ο(Fmlaβπ) is the set of all valid formulas, see fmla 34670. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ Fmla = (π β suc Ο β¦ dom ((β Sat β )βπ)) | ||
Definition | df-prv 34635* | Define the "proves" relation on a set. A wff is true in a model π if for every valuation π β (π βm Ο), the interpretation of the wff using the membership relation on π is true. Since β§ is defined in terms of the interpretations making the given formula true, it is not defined on the empty "model" π = β , since there are no interpretations. In particular, the empty set on the LHS of β§ should not be interpreted as the empty model. Statement prv0 34719 shows that our definition yields β β§π for all formulas, though of course the formula βπ₯π₯ = π₯ is not satisfied on the empty model. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ β§ = {β¨π, π’β© β£ (π Satβ π’) = (π βm Ο)} | ||
Theorem | goel 34636 | A "Godel-set of membership". The variables are identified by their indices (which are natural numbers), and the membership vi β vj is coded as β¨β , β¨π, πβ©β©. (Contributed by AV, 15-Sep-2023.) |
β’ ((πΌ β Ο β§ π½ β Ο) β (πΌβππ½) = β¨β , β¨πΌ, π½β©β©) | ||
Theorem | goelel3xp 34637 | A "Godel-set of membership" is a member of a doubled Cartesian product. (Contributed by AV, 16-Sep-2023.) |
β’ ((πΌ β Ο β§ π½ β Ο) β (πΌβππ½) β (Ο Γ (Ο Γ Ο))) | ||
Theorem | goeleq12bg 34638 | Two "Godel-set of membership" codes for two variables are equal iff the two corresponding variables are equal. (Contributed by AV, 8-Oct-2023.) |
β’ (((π β Ο β§ π β Ο) β§ (πΌ β Ο β§ π½ β Ο)) β ((πΌβππ½) = (πβππ) β (πΌ = π β§ π½ = π))) | ||
Theorem | gonafv 34639 | The "Godel-set for the Sheffer stroke NAND" for two formulas π΄ and π΅. (Contributed by AV, 16-Oct-2023.) |
β’ ((π΄ β π β§ π΅ β π) β (π΄βΌππ΅) = β¨1o, β¨π΄, π΅β©β©) | ||
Theorem | goaleq12d 34640 | Equality of the "Godel-set of universal quantification". (Contributed by AV, 18-Sep-2023.) |
β’ (π β π = π) & β’ (π β π΄ = π΅) β β’ (π β βπππ΄ = βπππ΅) | ||
Theorem | gonanegoal 34641 | The Godel-set for the Sheffer stroke NAND is not equal to the Godel-set of universal quantification. (Contributed by AV, 21-Oct-2023.) |
β’ (πβΌππ) β βπππ’ | ||
Theorem | satf 34642* | The satisfaction predicate as function over wff codes in the model π and the binary relation πΈ on π. (Contributed by AV, 14-Sep-2023.) |
β’ ((π β π β§ πΈ β π) β (π Sat πΈ) = (rec((π β V β¦ (π βͺ {β¨π₯, π¦β© β£ βπ’ β π (βπ£ β π (π₯ = ((1st βπ’)βΌπ(1st βπ£)) β§ π¦ = ((π βm Ο) β ((2nd βπ’) β© (2nd βπ£)))) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = {π β (π βm Ο) β£ βπ§ β π ({β¨π, π§β©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)}))})), {β¨π₯, π¦β© β£ βπ β Ο βπ β Ο (π₯ = (πβππ) β§ π¦ = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)})}) βΎ suc Ο)) | ||
Theorem | satfsucom 34643* | The satisfaction predicate for wff codes in the model π and the binary relation πΈ on π at an element of the successor of Ο. (Contributed by AV, 22-Sep-2023.) |
β’ ((π β π β§ πΈ β π β§ π β suc Ο) β ((π Sat πΈ)βπ) = (rec((π β V β¦ (π βͺ {β¨π₯, π¦β© β£ βπ’ β π (βπ£ β π (π₯ = ((1st βπ’)βΌπ(1st βπ£)) β§ π¦ = ((π βm Ο) β ((2nd βπ’) β© (2nd βπ£)))) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = {π β (π βm Ο) β£ βπ§ β π ({β¨π, π§β©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)}))})), {β¨π₯, π¦β© β£ βπ β Ο βπ β Ο (π₯ = (πβππ) β§ π¦ = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)})})βπ)) | ||
Theorem | satfn 34644 | The satisfaction predicate for wff codes in the model π and the binary relation πΈ on π is a function over suc Ο. (Contributed by AV, 6-Oct-2023.) |
β’ ((π β π β§ πΈ β π) β (π Sat πΈ) Fn suc Ο) | ||
Theorem | satom 34645* | The satisfaction predicate for wff codes in the model π and the binary relation πΈ on π at omega (Ο). (Contributed by AV, 6-Oct-2023.) |
β’ ((π β π β§ πΈ β π) β ((π Sat πΈ)βΟ) = βͺ π β Ο ((π Sat πΈ)βπ)) | ||
Theorem | satfvsucom 34646* | The satisfaction predicate as function over wff codes at a successor of Ο. (Contributed by AV, 22-Sep-2023.) |
β’ π = (π Sat πΈ) β β’ ((π β π β§ πΈ β π β§ π β suc Ο) β (πβπ) = (rec((π β V β¦ (π βͺ {β¨π₯, π¦β© β£ βπ’ β π (βπ£ β π (π₯ = ((1st βπ’)βΌπ(1st βπ£)) β§ π¦ = ((π βm Ο) β ((2nd βπ’) β© (2nd βπ£)))) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = {π β (π βm Ο) β£ βπ§ β π ({β¨π, π§β©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)}))})), {β¨π₯, π¦β© β£ βπ β Ο βπ β Ο (π₯ = (πβππ) β§ π¦ = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)})})βπ)) | ||
Theorem | satfv0 34647* | The value of the satisfaction predicate as function over wff codes at β . (Contributed by AV, 8-Oct-2023.) |
β’ π = (π Sat πΈ) β β’ ((π β π β§ πΈ β π) β (πββ ) = {β¨π₯, π¦β© β£ βπ β Ο βπ β Ο (π₯ = (πβππ) β§ π¦ = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)})}) | ||
Theorem | satfvsuclem1 34648* | Lemma 1 for satfvsuc 34650. (Contributed by AV, 8-Oct-2023.) |
β’ π = (π Sat πΈ) β β’ ((π β π β§ πΈ β π β§ π β Ο) β {β¨π₯, π¦β© β£ (βπ’ β (πβπ)(βπ£ β (πβπ)(π₯ = ((1st βπ’)βΌπ(1st βπ£)) β§ π¦ = ((π βm Ο) β ((2nd βπ’) β© (2nd βπ£)))) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = {π β (π βm Ο) β£ βπ§ β π ({β¨π, π§β©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)})) β§ π¦ β π« (π βm Ο))} β V) | ||
Theorem | satfvsuclem2 34649* | Lemma 2 for satfvsuc 34650. (Contributed by AV, 8-Oct-2023.) |
β’ π = (π Sat πΈ) β β’ ((π β π β§ πΈ β π β§ π β Ο) β {β¨π₯, π¦β© β£ βπ’ β (πβπ)(βπ£ β (πβπ)(π₯ = ((1st βπ’)βΌπ(1st βπ£)) β§ π¦ = ((π βm Ο) β ((2nd βπ’) β© (2nd βπ£)))) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = {π β (π βm Ο) β£ βπ§ β π ({β¨π, π§β©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)}))} β V) | ||
Theorem | satfvsuc 34650* | The value of the satisfaction predicate as function over wff codes at a successor. (Contributed by AV, 10-Oct-2023.) |
β’ π = (π Sat πΈ) β β’ ((π β π β§ πΈ β π β§ π β Ο) β (πβsuc π) = ((πβπ) βͺ {β¨π₯, π¦β© β£ βπ’ β (πβπ)(βπ£ β (πβπ)(π₯ = ((1st βπ’)βΌπ(1st βπ£)) β§ π¦ = ((π βm Ο) β ((2nd βπ’) β© (2nd βπ£)))) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = {π β (π βm Ο) β£ βπ§ β π ({β¨π, π§β©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)}))})) | ||
Theorem | satfv1lem 34651* | Lemma for satfv1 34652. (Contributed by AV, 9-Nov-2023.) |
β’ ((π β Ο β§ πΌ β Ο β§ π½ β Ο) β {π β (π βm Ο) β£ βπ§ β π ({β¨π, π§β©} βͺ (π βΎ (Ο β {π}))) β {π β (π βm Ο) β£ (πβπΌ)πΈ(πβπ½)}} = {π β (π βm Ο) β£ βπ§ β π if-(πΌ = π, if-(π½ = π, π§πΈπ§, π§πΈ(πβπ½)), if-(π½ = π, (πβπΌ)πΈπ§, (πβπΌ)πΈ(πβπ½)))}) | ||
Theorem | satfv1 34652* | The value of the satisfaction predicate as function over wff codes of height 1. (Contributed by AV, 9-Nov-2023.) |
β’ π = (π Sat πΈ) β β’ ((π β π β§ πΈ β π) β (πβ1o) = ((πββ ) βͺ {β¨π₯, π¦β© β£ βπ β Ο βπ β Ο (βπ β Ο βπ β Ο (π₯ = ((πβππ)βΌπ(πβππ)) β§ π¦ = {π β (π βm Ο) β£ (Β¬ (πβπ)πΈ(πβπ) β¨ Β¬ (πβπ)πΈ(πβπ))}) β¨ βπ β Ο (π₯ = βππ(πβππ) β§ π¦ = {π β (π βm Ο) β£ βπ§ β π if-(π = π, if-(π = π, π§πΈπ§, π§πΈ(πβπ)), if-(π = π, (πβπ)πΈπ§, (πβπ)πΈ(πβπ)))}))})) | ||
Theorem | satfsschain 34653 | The binary relation of a satisfaction predicate as function over wff codes is an increasing chain (with respect to inclusion). (Contributed by AV, 15-Oct-2023.) |
β’ π = (π Sat πΈ) β β’ (((π β π β§ πΈ β π) β§ (π΄ β Ο β§ π΅ β Ο)) β (π΅ β π΄ β (πβπ΅) β (πβπ΄))) | ||
Theorem | satfvsucsuc 34654* | The satisfaction predicate as function over wff codes of height (π + 1), expressed by the minimally necessary satisfaction predicates as function over wff codes of height π. (Contributed by AV, 21-Oct-2023.) |
β’ π = (π Sat πΈ) & β’ π΄ = ((π βm Ο) β ((2nd βπ’) β© (2nd βπ£))) & β’ π΅ = {π β (π βm Ο) β£ βπ§ β π ({β¨π, π§β©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)} β β’ ((π β π β§ πΈ β π β§ π β Ο) β (πβsuc suc π) = ((πβsuc π) βͺ {β¨π₯, π¦β© β£ (βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)(π₯ = ((1st βπ’)βΌπ(1st βπ£)) β§ π¦ = π΄) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = π΅)) β¨ βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))(π₯ = ((1st βπ’)βΌπ(1st βπ£)) β§ π¦ = π΄))})) | ||
Theorem | satfbrsuc 34655* | The binary relation of a satisfaction predicate as function over wff codes at a successor. (Contributed by AV, 13-Oct-2023.) |
β’ π = (π Sat πΈ) & β’ π = (πβπ) β β’ (((π β π β§ πΈ β π) β§ π β Ο β§ (π΄ β π β§ π΅ β π)) β (π΄(πβsuc π)π΅ β (π΄ππ΅ β¨ βπ’ β π (βπ£ β π (π΄ = ((1st βπ’)βΌπ(1st βπ£)) β§ π΅ = ((π βm Ο) β ((2nd βπ’) β© (2nd βπ£)))) β¨ βπ β Ο (π΄ = βππ(1st βπ’) β§ π΅ = {π β (π βm Ο) β£ βπ§ β π ({β¨π, π§β©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)}))))) | ||
Theorem | satfrel 34656 | The value of the satisfaction predicate as function over wff codes at a natural number is a relation. (Contributed by AV, 12-Oct-2023.) |
β’ ((π β π β§ πΈ β π β§ π β Ο) β Rel ((π Sat πΈ)βπ)) | ||
Theorem | satfdmlem 34657* | Lemma for satfdm 34658. (Contributed by AV, 12-Oct-2023.) |
β’ (((π β π β§ πΈ β π β§ π β Ο) β§ dom ((π Sat πΈ)βπ) = dom ((π Sat πΉ)βπ)) β (βπ’ β ((π Sat πΈ)βπ)(βπ£ β ((π Sat πΈ)βπ)π₯ = ((1st βπ’)βΌπ(1st βπ£)) β¨ βπ β Ο π₯ = βππ(1st βπ’)) β βπ β ((π Sat πΉ)βπ)(βπ β ((π Sat πΉ)βπ)π₯ = ((1st βπ)βΌπ(1st βπ)) β¨ βπ β Ο π₯ = βππ(1st βπ)))) | ||
Theorem | satfdm 34658* | The domain of the satisfaction predicate as function over wff codes does not depend on the model π and the binary relation πΈ on π. (Contributed by AV, 13-Oct-2023.) |
β’ (((π β π β§ πΈ β π) β§ (π β π β§ πΉ β π)) β βπ β Ο dom ((π Sat πΈ)βπ) = dom ((π Sat πΉ)βπ)) | ||
Theorem | satfrnmapom 34659 | The range of the satisfaction predicate as function over wff codes in any model π and any binary relation πΈ on π for a natural number π is a subset of the power set of all mappings from the natural numbers into the model π. (Contributed by AV, 13-Oct-2023.) |
β’ ((π β π β§ πΈ β π β§ π β Ο) β ran ((π Sat πΈ)βπ) β π« (π βm Ο)) | ||
Theorem | satfv0fun 34660 | The value of the satisfaction predicate as function over wff codes at β is a function. (Contributed by AV, 15-Oct-2023.) |
β’ ((π β π β§ πΈ β π) β Fun ((π Sat πΈ)ββ )) | ||
Theorem | satf0 34661* | The satisfaction predicate as function over wff codes in the empty model with an empty binary relation. (Contributed by AV, 14-Sep-2023.) |
β’ (β Sat β ) = (rec((π β V β¦ (π βͺ {β¨π₯, π¦β© β£ (π¦ = β β§ βπ’ β π (βπ£ β π π₯ = ((1st βπ’)βΌπ(1st βπ£)) β¨ βπ β Ο π₯ = βππ(1st βπ’)))})), {β¨π₯, π¦β© β£ (π¦ = β β§ βπ β Ο βπ β Ο π₯ = (πβππ))}) βΎ suc Ο) | ||
Theorem | satf0sucom 34662* | The satisfaction predicate as function over wff codes in the empty model with an empty binary relation at a successor of Ο. (Contributed by AV, 14-Sep-2023.) |
β’ (π β suc Ο β ((β Sat β )βπ) = (rec((π β V β¦ (π βͺ {β¨π₯, π¦β© β£ (π¦ = β β§ βπ’ β π (βπ£ β π π₯ = ((1st βπ’)βΌπ(1st βπ£)) β¨ βπ β Ο π₯ = βππ(1st βπ’)))})), {β¨π₯, π¦β© β£ (π¦ = β β§ βπ β Ο βπ β Ο π₯ = (πβππ))})βπ)) | ||
Theorem | satf00 34663* | The value of the satisfaction predicate as function over wff codes in the empty model with an empty binary relation at β . (Contributed by AV, 14-Sep-2023.) |
β’ ((β Sat β )ββ ) = {β¨π₯, π¦β© β£ (π¦ = β β§ βπ β Ο βπ β Ο π₯ = (πβππ))} | ||
Theorem | satf0suclem 34664* | Lemma for satf0suc 34665, sat1el2xp 34668 and fmlasuc0 34673. (Contributed by AV, 19-Sep-2023.) |
β’ ((π β π β§ π β π β§ π β π) β {β¨π₯, π¦β© β£ (π¦ = β β§ βπ’ β π (βπ£ β π π₯ = π΅ β¨ βπ€ β π π₯ = πΆ))} β V) | ||
Theorem | satf0suc 34665* | The value of the satisfaction predicate as function over wff codes in the empty model and the empty binary relation at a successor. (Contributed by AV, 19-Sep-2023.) |
β’ π = (β Sat β ) β β’ (π β Ο β (πβsuc π) = ((πβπ) βͺ {β¨π₯, π¦β© β£ (π¦ = β β§ βπ’ β (πβπ)(βπ£ β (πβπ)π₯ = ((1st βπ’)βΌπ(1st βπ£)) β¨ βπ β Ο π₯ = βππ(1st βπ’)))})) | ||
Theorem | satf0op 34666* | An element of a value of the satisfaction predicate as function over wff codes in the empty model and the empty binary relation expressed as ordered pair. (Contributed by AV, 19-Sep-2023.) |
β’ π = (β Sat β ) β β’ (π β Ο β (π β (πβπ) β βπ₯(π = β¨π₯, β β© β§ β¨π₯, β β© β (πβπ)))) | ||
Theorem | satf0n0 34667 | The value of the satisfaction predicate as function over wff codes in the empty model and the empty binary relation does not contain the empty set. (Contributed by AV, 19-Sep-2023.) |
β’ (π β Ο β β β ((β Sat β )βπ)) | ||
Theorem | sat1el2xp 34668* | The first component of an element of the value of the satisfaction predicate as function over wff codes in the empty model with an empty binary relation is a member of a doubled Cartesian product. (Contributed by AV, 17-Sep-2023.) |
β’ (π β Ο β βπ€ β ((β Sat β )βπ)βπβπ(1st βπ€) β (Ο Γ (π Γ π))) | ||
Theorem | fmlafv 34669 | The valid Godel formulas of height π is the domain of the value of the satisfaction predicate as function over wff codes in the empty model with an empty binary relation at π. (Contributed by AV, 15-Sep-2023.) |
β’ (π β suc Ο β (Fmlaβπ) = dom ((β Sat β )βπ)) | ||
Theorem | fmla 34670 | The set of all valid Godel formulas. (Contributed by AV, 20-Sep-2023.) |
β’ (FmlaβΟ) = βͺ π β Ο (Fmlaβπ) | ||
Theorem | fmla0 34671* | The valid Godel formulas of height 0 is the set of all formulas of the form vi β vj ("Godel-set of membership") coded as β¨β , β¨π, πβ©β©. (Contributed by AV, 14-Sep-2023.) |
β’ (Fmlaββ ) = {π₯ β V β£ βπ β Ο βπ β Ο π₯ = (πβππ)} | ||
Theorem | fmla0xp 34672 | The valid Godel formulas of height 0 is the set of all formulas of the form vi β vj ("Godel-set of membership") coded as β¨β , β¨π, πβ©β©. (Contributed by AV, 15-Sep-2023.) |
β’ (Fmlaββ ) = ({β } Γ (Ο Γ Ο)) | ||
Theorem | fmlasuc0 34673* | The valid Godel formulas of height (π + 1). (Contributed by AV, 18-Sep-2023.) |
β’ (π β Ο β (Fmlaβsuc π) = ((Fmlaβπ) βͺ {π₯ β£ βπ’ β ((β Sat β )βπ)(βπ£ β ((β Sat β )βπ)π₯ = ((1st βπ’)βΌπ(1st βπ£)) β¨ βπ β Ο π₯ = βππ(1st βπ’))})) | ||
Theorem | fmlafvel 34674 | A class is a valid Godel formula of height π iff it is the first component of a member of the value of the satisfaction predicate as function over wff codes in the empty model with an empty binary relation at π. (Contributed by AV, 19-Sep-2023.) |
β’ (π β Ο β (πΉ β (Fmlaβπ) β β¨πΉ, β β© β ((β Sat β )βπ))) | ||
Theorem | fmlasuc 34675* | The valid Godel formulas of height (π + 1), expressed by the valid Godel formulas of height π. (Contributed by AV, 20-Sep-2023.) |
β’ (π β Ο β (Fmlaβsuc π) = ((Fmlaβπ) βͺ {π₯ β£ βπ’ β (Fmlaβπ)(βπ£ β (Fmlaβπ)π₯ = (π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)})) | ||
Theorem | fmla1 34676* | The valid Godel formulas of height 1 is the set of all formulas of the form (πβΌππ) and βπππ with atoms π, π of the form π₯ β π¦. (Contributed by AV, 20-Sep-2023.) |
β’ (Fmlaβ1o) = (({β } Γ (Ο Γ Ο)) βͺ {π₯ β£ βπ β Ο βπ β Ο βπ β Ο (βπ β Ο π₯ = ((πβππ)βΌπ(πβππ)) β¨ π₯ = βππ(πβππ))}) | ||
Theorem | isfmlasuc 34677* | The characterization of a Godel formula of height at least 1. (Contributed by AV, 14-Oct-2023.) |
β’ ((π β Ο β§ πΉ β π) β (πΉ β (Fmlaβsuc π) β (πΉ β (Fmlaβπ) β¨ βπ’ β (Fmlaβπ)(βπ£ β (Fmlaβπ)πΉ = (π’βΌππ£) β¨ βπ β Ο πΉ = βπππ’)))) | ||
Theorem | fmlasssuc 34678 | The Godel formulas of height π are a subset of the Godel formulas of height π + 1. (Contributed by AV, 20-Oct-2023.) |
β’ (π β Ο β (Fmlaβπ) β (Fmlaβsuc π)) | ||
Theorem | fmlaomn0 34679 | The empty set is not a Godel formula of any height. (Contributed by AV, 21-Oct-2023.) |
β’ (π β Ο β β β (Fmlaβπ)) | ||
Theorem | fmlan0 34680 | The empty set is not a Godel formula. (Contributed by AV, 19-Nov-2023.) |
β’ β β (FmlaβΟ) | ||
Theorem | gonan0 34681 | The "Godel-set of NAND" is a Godel formula of at least height 1. (Contributed by AV, 21-Oct-2023.) |
β’ ((π΄βΌππ΅) β (Fmlaβπ) β π β β ) | ||
Theorem | goaln0 34682* | The "Godel-set of universal quantification" is a Godel formula of at least height 1. (Contributed by AV, 22-Oct-2023.) |
β’ (βπππ΄ β (Fmlaβπ) β π β β ) | ||
Theorem | gonarlem 34683* | Lemma for gonar 34684 (induction step). (Contributed by AV, 21-Oct-2023.) |
β’ (π β Ο β (((πβΌππ) β (Fmlaβsuc π) β (π β (Fmlaβsuc π) β§ π β (Fmlaβsuc π))) β ((πβΌππ) β (Fmlaβsuc suc π) β (π β (Fmlaβsuc suc π) β§ π β (Fmlaβsuc suc π))))) | ||
Theorem | gonar 34684* | If the "Godel-set of NAND" applied to classes is a Godel formula, the classes are also Godel formulas. Remark: The reverse is not valid for π΄ or π΅ being of the same height as the "Godel-set of NAND". (Contributed by AV, 21-Oct-2023.) |
β’ ((π β Ο β§ (πβΌππ) β (Fmlaβπ)) β (π β (Fmlaβπ) β§ π β (Fmlaβπ))) | ||
Theorem | goalrlem 34685* | Lemma for goalr 34686 (induction step). (Contributed by AV, 22-Oct-2023.) |
β’ (π β Ο β ((βπππ β (Fmlaβsuc π) β π β (Fmlaβsuc π)) β (βπππ β (Fmlaβsuc suc π) β π β (Fmlaβsuc suc π)))) | ||
Theorem | goalr 34686* | If the "Godel-set of universal quantification" applied to a class is a Godel formula, the class is also a Godel formula. Remark: The reverse is not valid for π΄ being of the same height as the "Godel-set of universal quantification". (Contributed by AV, 22-Oct-2023.) |
β’ ((π β Ο β§ βπππ β (Fmlaβπ)) β π β (Fmlaβπ)) | ||
Theorem | fmla0disjsuc 34687* | The set of valid Godel formulas of height 0 is disjoint with the formulas constructed from Godel-sets for the Sheffer stroke NAND and Godel-set of universal quantification. (Contributed by AV, 20-Oct-2023.) |
β’ ((Fmlaββ ) β© {π₯ β£ βπ’ β (Fmlaββ )(βπ£ β (Fmlaββ )π₯ = (π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)}) = β | ||
Theorem | fmlasucdisj 34688* | The valid Godel formulas of height (π + 1) is disjoint with the difference ((Fmlaβsuc suc π) β (Fmlaβsuc π)), expressed by formulas constructed from Godel-sets for the Sheffer stroke NAND and Godel-set of universal quantification based on the valid Godel formulas of height (π + 1). (Contributed by AV, 20-Oct-2023.) |
β’ (π β Ο β ((Fmlaβsuc π) β© {π₯ β£ (βπ’ β ((Fmlaβsuc π) β (Fmlaβπ))(βπ£ β (Fmlaβsuc π)π₯ = (π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’) β¨ βπ’ β (Fmlaβπ)βπ£ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (π’βΌππ£))}) = β ) | ||
Theorem | satfdmfmla 34689 | The domain of the satisfaction predicate as function over wff codes in any model π and any binary relation πΈ on π for a natural number π is the set of valid Godel formulas of height π. (Contributed by AV, 13-Oct-2023.) |
β’ ((π β π β§ πΈ β π β§ π β Ο) β dom ((π Sat πΈ)βπ) = (Fmlaβπ)) | ||
Theorem | satffunlem 34690 | Lemma for satffunlem1lem1 34691 and satffunlem2lem1 34693. (Contributed by AV, 27-Oct-2023.) |
β’ (((Fun π β§ (π β π β§ π β π) β§ (π’ β π β§ π£ β π)) β§ (π₯ = ((1st βπ )βΌπ(1st βπ)) β§ π¦ = ((π βm Ο) β ((2nd βπ ) β© (2nd βπ)))) β§ (π₯ = ((1st βπ’)βΌπ(1st βπ£)) β§ π€ = ((π βm Ο) β ((2nd βπ’) β© (2nd βπ£))))) β π¦ = π€) | ||
Theorem | satffunlem1lem1 34691* | Lemma for satffunlem1 34696. (Contributed by AV, 17-Oct-2023.) |
β’ (Fun ((π Sat πΈ)βπ) β Fun {β¨π₯, π¦β© β£ βπ’ β ((π Sat πΈ)βπ)(βπ£ β ((π Sat πΈ)βπ)(π₯ = ((1st βπ’)βΌπ(1st βπ£)) β§ π¦ = ((π βm Ο) β ((2nd βπ’) β© (2nd βπ£)))) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = {π β (π βm Ο) β£ βπ β π ({β¨π, πβ©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)}))}) | ||
Theorem | satffunlem1lem2 34692* | Lemma 2 for satffunlem1 34696. (Contributed by AV, 23-Oct-2023.) |
β’ ((π β π β§ πΈ β π) β (dom ((π Sat πΈ)ββ ) β© dom {β¨π₯, π¦β© β£ βπ’ β ((π Sat πΈ)ββ )(βπ£ β ((π Sat πΈ)ββ )(π₯ = ((1st βπ’)βΌπ(1st βπ£)) β§ π¦ = ((π βm Ο) β ((2nd βπ’) β© (2nd βπ£)))) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = {π β (π βm Ο) β£ βπ β π ({β¨π, πβ©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)}))}) = β ) | ||
Theorem | satffunlem2lem1 34693* | Lemma 1 for satffunlem2 34697. (Contributed by AV, 28-Oct-2023.) |
β’ π = (π Sat πΈ) & β’ π΄ = ((π βm Ο) β ((2nd βπ’) β© (2nd βπ£))) & β’ π΅ = {π β (π βm Ο) β£ βπ§ β π ({β¨π, π§β©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)} β β’ ((Fun (πβsuc π) β§ (πβπ) β (πβsuc π)) β Fun {β¨π₯, π¦β© β£ (βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)(π₯ = ((1st βπ’)βΌπ(1st βπ£)) β§ π¦ = π΄) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = π΅)) β¨ βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))(π₯ = ((1st βπ’)βΌπ(1st βπ£)) β§ π¦ = π΄))}) | ||
Theorem | dmopab3rexdif 34694* | The domain of an ordered pair class abstraction with three nested restricted existential quantifiers with differences. (Contributed by AV, 25-Oct-2023.) |
β’ ((βπ’ β π (βπ£ β π π΅ β π β§ βπ β πΌ π· β π) β§ π β π) β dom {β¨π₯, π¦β© β£ (βπ’ β (π β π)(βπ£ β π (π₯ = π΄ β§ π¦ = π΅) β¨ βπ β πΌ (π₯ = πΆ β§ π¦ = π·)) β¨ βπ’ β π βπ£ β (π β π)(π₯ = π΄ β§ π¦ = π΅))} = {π₯ β£ (βπ’ β (π β π)(βπ£ β π π₯ = π΄ β¨ βπ β πΌ π₯ = πΆ) β¨ βπ’ β π βπ£ β (π β π)π₯ = π΄)}) | ||
Theorem | satffunlem2lem2 34695* | Lemma 2 for satffunlem2 34697. (Contributed by AV, 27-Oct-2023.) |
β’ π = (π Sat πΈ) & β’ π΄ = ((π βm Ο) β ((2nd βπ’) β© (2nd βπ£))) & β’ π΅ = {π β (π βm Ο) β£ βπ§ β π ({β¨π, π§β©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)} β β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (dom (πβsuc π) β© dom {β¨π₯, π¦β© β£ (βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)(π₯ = ((1st βπ’)βΌπ(1st βπ£)) β§ π¦ = π΄) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = π΅)) β¨ βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))(π₯ = ((1st βπ’)βΌπ(1st βπ£)) β§ π¦ = π΄))}) = β ) | ||
Theorem | satffunlem1 34696 | Lemma 1 for satffun 34698: induction basis. (Contributed by AV, 28-Oct-2023.) |
β’ ((π β π β§ πΈ β π) β Fun ((π Sat πΈ)βsuc β )) | ||
Theorem | satffunlem2 34697 | Lemma 2 for satffun 34698: induction step. (Contributed by AV, 28-Oct-2023.) |
β’ ((π β Ο β§ (π β π β§ πΈ β π)) β (Fun ((π Sat πΈ)βsuc π) β Fun ((π Sat πΈ)βsuc suc π))) | ||
Theorem | satffun 34698 | The value of the satisfaction predicate as function over wff codes at a natural number is a function. (Contributed by AV, 28-Oct-2023.) |
β’ ((π β π β§ πΈ β π β§ π β Ο) β Fun ((π Sat πΈ)βπ)) | ||
Theorem | satff 34699 | The satisfaction predicate as function over wff codes in the model π and the binary relation πΈ on π. (Contributed by AV, 28-Oct-2023.) |
β’ ((π β π β§ πΈ β π β§ π β Ο) β ((π Sat πΈ)βπ):(Fmlaβπ)βΆπ« (π βm Ο)) | ||
Theorem | satfun 34700 | The satisfaction predicate as function over wff codes in the model π and the binary relation πΈ on π. (Contributed by AV, 29-Oct-2023.) |
β’ ((π β π β§ πΈ β π) β ((π Sat πΈ)βΟ):(FmlaβΟ)βΆπ« (π βm Ο)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |