Its for soundness theorem. I need to prove that the axioms (∀x)A -> A[t/x] its valid in constant domain semantics. I assume theres a world in a arbitrary model within (∀x)A -> A[t/x] its false and i search a contraddiction. (∀x)A -> A[t/x] its false when (∀x)A its true and A[t/x] its false. (∀x)A its true when A its true for each objects o in U (or D, the domain) that the valuaction function v assigns to the variable, but i dont understand how to explain that A[t/x] its false in logic sintax.
4
-
A(t) is false for a valuation when the objects assigned to term t does not belong to subset of the domain assigned to predicate A by the interpretation.– Mauro ALLEGRANZASep 16 at 18:26
-
And A(t) will never be false if you have (∀x)A(x) with a constant domain across all possible worlds.– BumbleSep 16 at 23:11
-
1You seem confused, we can never prove axioms but prove theorems founded upon axioms. You're just trying to prove soundness of the UI rule for constant domain QML with a probabilist reading instead of varying domain such as expanding or contracting ones. To syntactically prove soundness in general you need induction on the length/complexity of a generic proof including step of any nested subproof. As for your centrally concerned syntactic expression for A[t/x] being false is ⊨¬A(t) were t is any term, which contradicts the very last step entailment ⊨(∀x)A simply by quantifier's definition...– Double KnotSep 17 at 6:54
-
I understand thank you so much for the answer, i thought was something more difficult... But can i ask u something? I always read in books "induction on the lenght or complexity of the formula", but not having a mathematical background i never understand this point. Can u explain very quicly or send me to some beginner friendly literature?– davide_cavaSep 17 at 8:29
Add a comment
|