Home | Metamath
Proof Explorer Theorem List (p. 327 of 450) | < 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: | Metamath Proof Explorer
(1-28694) |
Hilbert Space Explorer
(28695-30217) |
Users' Mathboxes
(30218-44905) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | satfsucom 32601* | 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 32602 | 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 32603* | 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 32604* | 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 32605* | The value of the satisfaction predicate as function over wff codes at ∅. (Contributed by AV, 8-Oct-2023.) |
⊢ 𝑆 = (𝑀 Sat 𝐸) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})}) | ||
Theorem | satfvsuclem1 32606* | Lemma 1 for satfvsuc 32608. (Contributed by AV, 8-Oct-2023.) |
⊢ 𝑆 = (𝑀 Sat 𝐸) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → {〈𝑥, 𝑦〉 ∣ (∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑m ω))} ∈ V) | ||
Theorem | satfvsuclem2 32607* | Lemma 2 for satfvsuc 32608. (Contributed by AV, 8-Oct-2023.) |
⊢ 𝑆 = (𝑀 Sat 𝐸) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))} ∈ V) | ||
Theorem | satfvsuc 32608* | 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 32609* | Lemma for satfv1 32610. (Contributed by AV, 9-Nov-2023.) |
⊢ ((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) → {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ {𝑏 ∈ (𝑀 ↑m ω) ∣ (𝑏‘𝐼)𝐸(𝑏‘𝐽)}} = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑁, if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))}) | ||
Theorem | satfv1 32610* | 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 32611 | 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 32612* | 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 32613* | 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 32614 | 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 32615* | Lemma for satfdm 32616. (Contributed by AV, 12-Oct-2023.) |
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) → ∃𝑎 ∈ ((𝑁 Sat 𝐹)‘𝑌)(∃𝑏 ∈ ((𝑁 Sat 𝐹)‘𝑌)𝑥 = ((1st ‘𝑎)⊼𝑔(1st ‘𝑏)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑎)))) | ||
Theorem | satfdm 32616* | 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 32617 | 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 32618 | 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 32619* | 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 32620* | 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 32621* | 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 32622* | Lemma for satf0suc 32623, sat1el2xp 32626 and fmlasuc0 32631. (Contributed by AV, 19-Sep-2023.) |
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑋 (∃𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃𝑤 ∈ 𝑍 𝑥 = 𝐶))} ∈ V) | ||
Theorem | satf0suc 32623* | 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 32624* | 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 32625 | 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 32626* | 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 32627 | 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 32628 | The set of all valid Godel formulas. (Contributed by AV, 20-Sep-2023.) |
⊢ (Fmla‘ω) = ∪ 𝑛 ∈ ω (Fmla‘𝑛) | ||
Theorem | fmla0 32629* | 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 32630 | 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 32631* | The valid Godel formulas of height (𝑁 + 1). (Contributed by AV, 18-Sep-2023.) |
⊢ (𝑁 ∈ ω → (Fmla‘suc 𝑁) = ((Fmla‘𝑁) ∪ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))})) | ||
Theorem | fmlafvel 32632 | 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 32633* | 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 32634* | 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 32635* | The characterization of a Godel formula of height at least 1. (Contributed by AV, 14-Oct-2023.) |
⊢ ((𝑁 ∈ ω ∧ 𝐹 ∈ 𝑉) → (𝐹 ∈ (Fmla‘suc 𝑁) ↔ (𝐹 ∈ (Fmla‘𝑁) ∨ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝐹 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝐹 = ∀𝑔𝑖𝑢)))) | ||
Theorem | fmlasssuc 32636 | 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 32637 | The empty set is not a Godel formula of any height. (Contributed by AV, 21-Oct-2023.) |
⊢ (𝑁 ∈ ω → ∅ ∉ (Fmla‘𝑁)) | ||
Theorem | fmlan0 32638 | The empty set is not a Godel formula. (Contributed by AV, 19-Nov-2023.) |
⊢ ∅ ∉ (Fmla‘ω) | ||
Theorem | gonan0 32639 | The "Godel-set of NAND" is a Godel formula of at least height 1. (Contributed by AV, 21-Oct-2023.) |
⊢ ((𝐴⊼𝑔𝐵) ∈ (Fmla‘𝑁) → 𝑁 ≠ ∅) | ||
Theorem | goaln0 32640* | The "Godel-set of universal quantification" is a Godel formula of at least height 1. (Contributed by AV, 22-Oct-2023.) |
⊢ (∀𝑔𝑖𝐴 ∈ (Fmla‘𝑁) → 𝑁 ≠ ∅) | ||
Theorem | gonarlem 32641* | Lemma for gonar 32642 (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 32642* | 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 32643* | Lemma for goalr 32644 (induction step). (Contributed by AV, 22-Oct-2023.) |
⊢ (𝑁 ∈ ω → ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁)) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑁) → 𝑎 ∈ (Fmla‘suc suc 𝑁)))) | ||
Theorem | goalr 32644* | 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 32645* | 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 32646* | 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 32647 | 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 32648 | Lemma for satffunlem1lem1 32649 and satffunlem2lem1 32651. (Contributed by AV, 27-Oct-2023.) |
⊢ (((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑠) ∩ (2nd ‘𝑟)))) ∧ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑤 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))))) → 𝑦 = 𝑤) | ||
Theorem | satffunlem1lem1 32649* | Lemma for satffunlem1 32654. (Contributed by AV, 17-Oct-2023.) |
⊢ (Fun ((𝑀 Sat 𝐸)‘𝑁) → Fun {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ ∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}) | ||
Theorem | satffunlem1lem2 32650* | Lemma 2 for satffunlem1 32654. (Contributed by AV, 23-Oct-2023.) |
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (dom ((𝑀 Sat 𝐸)‘∅) ∩ dom {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ ∀𝑗 ∈ 𝑀 ({〈𝑖, 𝑗〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}) = ∅) | ||
Theorem | satffunlem2lem1 32651* | Lemma 1 for satffunlem2 32655. (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 32652* | 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 32653* | Lemma 2 for satffunlem2 32655. (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 32654 | Lemma 1 for satffun 32656: induction basis. (Contributed by AV, 28-Oct-2023.) |
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → Fun ((𝑀 Sat 𝐸)‘suc ∅)) | ||
Theorem | satffunlem2 32655 | Lemma 2 for satffun 32656: induction step. (Contributed by AV, 28-Oct-2023.) |
⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) → Fun ((𝑀 Sat 𝐸)‘suc suc 𝑁))) | ||
Theorem | satffun 32656 | 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 32657 | 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 32658 | 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 ω)) | ||
Theorem | satfvel 32659 | An element of the value of the satisfaction predicate as function over wff codes in the model 𝑀 and the binary relation 𝐸 on 𝑀 at the code 𝑈 for a wff using ∈ , ⊼ , ∀ is a valuation 𝑆:ω⟶𝑀 of the variables (v0 = (𝑆‘∅), v1 = (𝑆‘1o), etc.) so that 𝑈 is true under the assignment 𝑆. (Contributed by AV, 29-Oct-2023.) |
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑈 ∈ (Fmla‘ω) ∧ 𝑆 ∈ (((𝑀 Sat 𝐸)‘ω)‘𝑈)) → 𝑆:ω⟶𝑀) | ||
Theorem | satfv0fvfmla0 32660* | The value of the satisfaction predicate as function over a wff code at ∅. (Contributed by AV, 2-Nov-2023.) |
⊢ 𝑆 = (𝑀 Sat 𝐸) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑋 ∈ (Fmla‘∅)) → ((𝑆‘∅)‘𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st ‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd ‘𝑋)))}) | ||
Theorem | satefv 32661 | The simplified satisfaction predicate as function over wff codes in the model 𝑀 at the code 𝑈. (Contributed by AV, 30-Oct-2023.) |
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑈 ∈ 𝑊) → (𝑀 Sat∈ 𝑈) = (((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω)‘𝑈)) | ||
Theorem | sate0 32662 | The simplified satisfaction predicate for any wff code over an empty model. (Contributed by AV, 6-Oct-2023.) (Revised by AV, 5-Nov-2023.) |
⊢ (𝑈 ∈ 𝑉 → (∅ Sat∈ 𝑈) = (((∅ Sat ∅)‘ω)‘𝑈)) | ||
Theorem | satef 32663 | The simplified satisfaction predicate as function over wff codes over an empty model. (Contributed by AV, 30-Oct-2023.) |
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑈 ∈ (Fmla‘ω) ∧ 𝑆 ∈ (𝑀 Sat∈ 𝑈)) → 𝑆:ω⟶𝑀) | ||
Theorem | sate0fv0 32664 | A simplified satisfaction predicate as function over wff codes over an empty model is an empty set. (Contributed by AV, 31-Oct-2023.) |
⊢ (𝑈 ∈ (Fmla‘ω) → (𝑆 ∈ (∅ Sat∈ 𝑈) → 𝑆 = ∅)) | ||
Theorem | satefvfmla0 32665* | The simplified satisfaction predicate for wff codes of height 0. (Contributed by AV, 4-Nov-2023.) |
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) → (𝑀 Sat∈ 𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st ‘(2nd ‘𝑋))) ∈ (𝑎‘(2nd ‘(2nd ‘𝑋)))}) | ||
Theorem | sategoelfvb 32666 | Characterization of a valuation 𝑆 of a simplified satisfaction predicate for a Godel-set of membership. (Contributed by AV, 5-Nov-2023.) |
⊢ 𝐸 = (𝑀 Sat∈ (𝐴∈𝑔𝐵)) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝑆 ∈ 𝐸 ↔ (𝑆 ∈ (𝑀 ↑m ω) ∧ (𝑆‘𝐴) ∈ (𝑆‘𝐵)))) | ||
Theorem | sategoelfv 32667 | Condition of a valuation 𝑆 of a simplified satisfaction predicate for a Godel-set of membership: The sets in model 𝑀 corresponding to the variables 𝐴 and 𝐵 under the assignment of 𝑆 are in a membership relation in 𝑀. (Contributed by AV, 5-Nov-2023.) |
⊢ 𝐸 = (𝑀 Sat∈ (𝐴∈𝑔𝐵)) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝑆 ∈ 𝐸) → (𝑆‘𝐴) ∈ (𝑆‘𝐵)) | ||
Theorem | ex-sategoelel 32668* | Example of a valuation of a simplified satisfaction predicate for a Godel-set of membership. (Contributed by AV, 5-Nov-2023.) |
⊢ 𝐸 = (𝑀 Sat∈ (𝐴∈𝑔𝐵)) & ⊢ 𝑆 = (𝑥 ∈ ω ↦ if(𝑥 = 𝐴, 𝑍, if(𝑥 = 𝐵, 𝒫 𝑍, ∅))) ⇒ ⊢ (((𝑀 ∈ WUni ∧ 𝑍 ∈ 𝑀) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ≠ 𝐵)) → 𝑆 ∈ 𝐸) | ||
Theorem | ex-sategoel 32669* | Instance of sategoelfv 32667 for the example of a valuation of a simplified satisfaction predicate for a Godel-set of membership. (Contributed by AV, 5-Nov-2023.) |
⊢ 𝐸 = (𝑀 Sat∈ (𝐴∈𝑔𝐵)) & ⊢ 𝑆 = (𝑥 ∈ ω ↦ if(𝑥 = 𝐴, 𝑍, if(𝑥 = 𝐵, 𝒫 𝑍, ∅))) ⇒ ⊢ (((𝑀 ∈ WUni ∧ 𝑍 ∈ 𝑀) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ≠ 𝐵)) → (𝑆‘𝐴) ∈ (𝑆‘𝐵)) | ||
Theorem | satfv1fvfmla1 32670* | The value of the satisfaction predicate at two Godel-sets of membership combined with a Godel-set for NAND. (Contributed by AV, 17-Nov-2023.) |
⊢ 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿)) ⇒ ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (((𝑀 Sat 𝐸)‘1o)‘𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬ (𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}) | ||
Theorem | 2goelgoanfmla1 32671 | Two Godel-sets of membership combined with a Godel-set for NAND is a Godel formula of height 1. (Contributed by AV, 17-Nov-2023.) |
⊢ 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿)) ⇒ ⊢ (((𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 𝑋 ∈ (Fmla‘1o)) | ||
Theorem | satefvfmla1 32672* | The simplified satisfaction predicate at two Godel-sets of membership combined with a Godel-set for NAND. (Contributed by AV, 17-Nov-2023.) |
⊢ 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿)) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (𝑀 Sat∈ 𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬ (𝑎‘𝐼) ∈ (𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾) ∈ (𝑎‘𝐿))}) | ||
Theorem | ex-sategoelelomsuc 32673* | Example of a valuation of a simplified satisfaction predicate over the ordinal numbers as model for a Godel-set of membership using the properties of a successor: (𝑆‘2o) = 𝑍 ∈ suc 𝑍 = (𝑆‘2o). Remark: the indices 1o and 2o are intentionally reversed to distinguish them from elements of the model: (2o∈𝑔1o) should not be confused with 2o ∈ 1o, which is false. (Contributed by AV, 19-Nov-2023.) |
⊢ 𝑆 = (𝑥 ∈ ω ↦ if(𝑥 = 2o, 𝑍, suc 𝑍)) ⇒ ⊢ (𝑍 ∈ ω → 𝑆 ∈ (ω Sat∈ (2o∈𝑔1o))) | ||
Theorem | ex-sategoelel12 32674 | Example of a valuation of a simplified satisfaction predicate over a proper pair (of ordinal numbers) as model for a Godel-set of membership using the properties of a successor: (𝑆‘2o) = 1o ∈ 2o = (𝑆‘2o). Remark: the indices 1o and 2o are intentionally reversed to distinguish them from elements of the model: (2o∈𝑔1o) should not be confused with 2o ∈ 1o, which is false. (Contributed by AV, 19-Nov-2023.) |
⊢ 𝑆 = (𝑥 ∈ ω ↦ if(𝑥 = 2o, 1o, 2o)) ⇒ ⊢ 𝑆 ∈ ({1o, 2o} Sat∈ (2o∈𝑔1o)) | ||
Theorem | prv 32675 | The "proves" relation on a set. A wff encoded as 𝑈 is true in a model 𝑀 iff for every valuation 𝑠 ∈ (𝑀 ↑m ω), the interpretation of the wff using the membership relation on 𝑀 is true. (Contributed by AV, 5-Nov-2023.) |
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑈 ∈ 𝑊) → (𝑀⊧𝑈 ↔ (𝑀 Sat∈ 𝑈) = (𝑀 ↑m ω))) | ||
Theorem | elnanelprv 32676 | The wff (𝐴 ∈ 𝐵 ⊼ 𝐵 ∈ 𝐴) encoded as ((𝐴∈𝑔𝐵) ⊼𝑔(𝐵∈𝑔𝐴)) is true in any model 𝑀. This is the model theoretic proof of elnanel 9069. (Contributed by AV, 5-Nov-2023.) |
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝑀⊧((𝐴∈𝑔𝐵)⊼𝑔(𝐵∈𝑔𝐴))) | ||
Theorem | prv0 32677 | Every wff encoded as 𝑈 is true in an "empty model" (𝑀 = ∅). 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, because ∃𝑥𝑥 = 𝑥 is not satisfied on the empty model. (Contributed by AV, 19-Nov-2023.) |
⊢ (𝑈 ∈ (Fmla‘ω) → ∅⊧𝑈) | ||
Theorem | prv1n 32678 | No wff encoded as a Godel-set of membership is true in a model with only one element. (Contributed by AV, 19-Nov-2023.) |
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ¬ {𝑋}⊧(𝐼∈𝑔𝐽)) | ||
Syntax | cgon 32679 | The Godel-set of negation. (Note that this is not a wff.) |
class ¬𝑔𝑈 | ||
Syntax | cgoa 32680 | The Godel-set of conjunction. |
class ∧𝑔 | ||
Syntax | cgoi 32681 | The Godel-set of implication. |
class →𝑔 | ||
Syntax | cgoo 32682 | The Godel-set of disjunction. |
class ∨𝑔 | ||
Syntax | cgob 32683 | The Godel-set of equivalence. |
class ↔𝑔 | ||
Syntax | cgoq 32684 | The Godel-set of equality. |
class =𝑔 | ||
Syntax | cgox 32685 | The Godel-set of existential quantification. (Note that this is not a wff.) |
class ∃𝑔𝑁𝑈 | ||
Definition | df-gonot 32686 | Define the Godel-set of negation. Here the argument 𝑈 is also a Godel-set corresponding to smaller formulas. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ ¬𝑔𝑈 = (𝑈⊼𝑔𝑈) | ||
Definition | df-goan 32687* | Define the Godel-set of conjunction. Here the arguments 𝑈 and 𝑉 are also Godel-sets corresponding to smaller formulas. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ ∧𝑔 = (𝑢 ∈ V, 𝑣 ∈ V ↦ ¬𝑔(𝑢⊼𝑔𝑣)) | ||
Definition | df-goim 32688* | Define the Godel-set of implication. Here the arguments 𝑈 and 𝑉 are also Godel-sets corresponding to smaller formulas. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ →𝑔 = (𝑢 ∈ V, 𝑣 ∈ V ↦ (𝑢⊼𝑔¬𝑔𝑣)) | ||
Definition | df-goor 32689* | Define the Godel-set of disjunction. Here the arguments 𝑈 and 𝑉 are also Godel-sets corresponding to smaller formulas. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ ∨𝑔 = (𝑢 ∈ V, 𝑣 ∈ V ↦ (¬𝑔𝑢 →𝑔 𝑣)) | ||
Definition | df-gobi 32690* | Define the Godel-set of equivalence. Here the arguments 𝑈 and 𝑉 are also Godel-sets corresponding to smaller formulas. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ ↔𝑔 = (𝑢 ∈ V, 𝑣 ∈ V ↦ ((𝑢 →𝑔 𝑣)∧𝑔(𝑣 →𝑔 𝑢))) | ||
Definition | df-goeq 32691* | Define the Godel-set of equality. Here the arguments 𝑥 = 〈𝑁, 𝑃〉 correspond to vN and vP , so (∅=𝑔1o) actually means v0 = v1 , not 0 = 1. Here we use the trick mentioned in ax-ext 2793 to introduce equality as a defined notion in terms of ∈𝑔. The expression suc (𝑢 ∪ 𝑣) = max (𝑢, 𝑣) + 1 here is a convenient way of getting a dummy variable distinct from 𝑢 and 𝑣. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ =𝑔 = (𝑢 ∈ ω, 𝑣 ∈ ω ↦ ⦋suc (𝑢 ∪ 𝑣) / 𝑤⦌∀𝑔𝑤((𝑤∈𝑔𝑢) ↔𝑔 (𝑤∈𝑔𝑣))) | ||
Definition | df-goex 32692 | Define the Godel-set of existential 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.) |
⊢ ∃𝑔𝑁𝑈 = ¬𝑔∀𝑔𝑁¬𝑔𝑈 | ||
Syntax | cgze 32693 | The Axiom of Extensionality. |
class AxExt | ||
Syntax | cgzr 32694 | The Axiom Scheme of Replacement. |
class AxRep | ||
Syntax | cgzp 32695 | The Axiom of Power Sets. |
class AxPow | ||
Syntax | cgzu 32696 | The Axiom of Unions. |
class AxUn | ||
Syntax | cgzg 32697 | The Axiom of Regularity. |
class AxReg | ||
Syntax | cgzi 32698 | The Axiom of Infinity. |
class AxInf | ||
Syntax | cgzf 32699 | The set of models of ZF. |
class ZF | ||
Definition | df-gzext 32700 | The Godel-set version of the Axiom of Extensionality. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ AxExt = (∀𝑔2o((2o∈𝑔∅) ↔𝑔 (2o∈𝑔1o)) →𝑔 (∅=𝑔1o)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |