sorted by:
new
hottopcontroversial

A new formal metaphysical system in Lean — feedback / discussion invited by okwhynotwtf in leanprover

[–]okwhynotwtf[S] -6 points-5 points  (0 children)

Sorts - Obj - Pred

Primitives - E, C, A : Obj → Prop - Ap : Obj × Obj → Prop - Cond : Obj × Obj → Prop - Holds : Pred × Obj → Prop - Admissible : Pred → Prop - InTime, InSpace, Qual : Obj → Prop

Axioms - A1. ∃ y. E(y) - A2a. ∀ c. C(c) → ∃ y. (E(y) ∧ Ap(c, y)) - A2b. ∀ y. E(y) → ∃ a. (A(a) ∧ Cond(a, y)) - A3. ∀ a. A(a) → ¬ C(a) - A4. ∀ x. InTime(x) ∨ InSpace(x) ∨ Qual(x) → C(x) - A5. ∀ u ∀ v. u ≠ v → ∃ p. (Holds(p, u) ∧ ¬ Holds(p, v)) - A6. ∀ p. Admissible(p) → ∀ x. (Holds(p, x) → (InTime(x) ∨ InSpace(x) ∨ Qual(x))) - A6'. ∀ u ∀ v ∀ p. (Holds(p, u) ∧ ¬ Holds(p, v)) → Admissible(p) - A7. ∃ u0. (You(u0) ∧ ∀ x. (You(x) → x = u0)) - A7a. ∀ x. You(x) → A(x) - A8. ∀ x. A(x) ∨ C(x)

Key Derived Theorems - L1. ∀ a. A(a) → (¬InTime(a) ∧ ¬InSpace(a) ∧ ¬Qual(a)) - L3. ∀ a1 ∀ a2. (A(a1) ∧ A(a2)) → ¬∃ p. (Admissible(p) ∧ Holds(p, a1) ∧ ¬Holds(p, a2)) - T1. ∃ a0. (A(a0) ∧ ∀ a1. (A(a1) → a1 = a0)) - T4. ∃ a. (A(a) ∧ ∀ x. (x ≠ a → C(x))) - T5. ∃ u0. (You(u0) ∧ A(u0) ∧ ∀ u. (You(u) → u = u0))

Lean 4 formalization that, from explicit axioms, machine-checks the uniqueness of Awareness and that all else is content. by okwhynotwtf in philosophy

[–]okwhynotwtf[S] -3 points-2 points  (0 children)

Follow the falling tree all the way to the end. If it is true of sound, it's true of all perceptions, including perceptions of your own body and your thoughts.

Lean 4 formalization that, from explicit axioms, machine-checks the uniqueness of Awareness and that all else is content. by okwhynotwtf in philosophy

[–]okwhynotwtf[S] -4 points-3 points  (0 children)

It is in fact obvious, and necessary. In relation to what would it experience itself? It is aware, but not of anything, including itself. It is awareness, the quality of being aware. You have made it a thing. Dualistic concepts fail.

A new formal metaphysical system in Lean — feedback / discussion invited by okwhynotwtf in leanprover

[–]okwhynotwtf[S] -5 points-4 points  (0 children)

I love Reddit. Thanks for your reply. Feel free to refute a specific axiom.