0

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. Sep 16, 2023 at 18:26
  • And A(t) will never be false if you have (∀x)A(x) with a constant domain across all possible worlds.
    – Bumble
    Sep 16, 2023 at 23:11
  • 1
    You 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... Sep 17, 2023 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? Sep 17, 2023 at 8:29

0

You must log in to answer this question.

Browse other questions tagged .