How to Prove Soundness for Proof Trees | Logic tutorial | Attic Philosophy

Поделиться
HTML-код
  • Опубликовано: 12 дек 2024

Комментарии • 14

  • @AtticPhilosophy
    @AtticPhilosophy  2 года назад

    Proving soundness is actually a lot easier than it looks at first! Got a question? Leave me a comment below.

  • @pfroncole1
    @pfroncole1 Год назад

    Regarding the Ttree method and soundness in FOL, would you agree with: there are, essentially, 2 rules of inference - the ^ and v rule (iterations of the 2 are of no significant difference). Both rules are sound by truth table reference. We assume a satisfiable set of premises ( we can consider the reductio assumption to be a premise) to show that IF we have such a set, then its relevant truth tree must end with at least one open branch, which means that being that an open branch is a proof, it entails a model of the premises.
    Proof: 1) We translate every sentence in the premises to an and or an v equivalent sentence. Simple Atomic sentences we translate to ^ sentences (they can also be translated to v sentences, but if they are, they must be listed immediately following the trunk of the tree before all other v sentences that are not of the same type). 2)All existential generalizations most usually instantiate to and statements but in an odd case may translate to an v. All universal generalizations translate to v statements. 3) All and statements we organize into a vertical list of any order we like which forms the trunk of our tree. Every sentence listed in the trunk is true by reference to the satisfiability of the premises so the trunk is "open"..Now, being that all we have left are or statements that are the equivalents of OR statements in the premises, it follows that every OR we attach to the trunk and onward must be open, hence there is at least one branch open through the tree and our proof entails a model ..The 0 complexity sentences of the proof entail a model for any open branch, and we have AT LEAST one open branch per proof.
    The main difference between sentential and FOL in showing that a proof of an open branch entails a model is that FOl Will usually have more OR statements attached to the tree than in the case of propositional proofs (depends on the number of constants and the number of universal generalizations ) but any OR statements from the premises are true no matter how many the case is.
    ASIDE: what if we have only a set of all ^ and statements? Well, then we have a simple open trunk. In fact a set of all true premises must be open (arranged vertically) if each individual sentence is true in the set, so it's trivial to see the openess of satisfiable sets..BUT there's no way to know the model(s) without doing the proof(s). And the same goes for any set of all true OR statements.

    • @AtticPhilosophy
      @AtticPhilosophy  Год назад

      I wouldn't say the FOL tree rules are just the & and v rules. The quantifier rules are quite different, for example. You can (just about) treat universal statements AxFx as infinite conjunctions, and existentials ExFx as infinite disjunctions, but you don't want infinite sentences in tree proofs!

    • @pfroncole1
      @pfroncole1 Год назад

      @@AtticPhilosophy Yes, it's a given that in Truth Trees for FOL, rules specific to Fol (restriction rules) have to be followed ..like existential instantiation of exactly 1 constant per generalization (can use variables as well to cut down on symbols) and universal after existential and for every constant in a branch..but those rules don't really add anything to the various ^ and v rules?

    • @pfroncole1
      @pfroncole1 Год назад

      Being that all proofs have to be finite, it's hard to see how to work infinite domains into trees to model?

    • @pfroncole1
      @pfroncole1 Год назад

      @@AtticPhilosophy but (X) (Fx > Gx) legitimately translates to (X) ( -Fx v Gx ) as the UG instantiation rule in FOL.. and the Existential Gen. Translates to an ^ generally.. if not, then an v also. Every single Fol problem Is worked out this way.

  • @jupironnie1
    @jupironnie1 2 года назад

    Please consider a new video showing compliance to Soundness using Truth tables. I am aware that Trees gives equal results to Tables and I dig (tables) Tables. I just want to understand why Completeness is of any use. Thx

    • @AtticPhilosophy
      @AtticPhilosophy  2 года назад +1

      Truth-tables are a kind of semantics, whereas proof trees are a kind of proof. Soundness & completeness are about how proof systems (e.g. trees) line up with the semantics (e.g. truth tables). So it doesn't really make sense to ask about whether truth tables are sound or complete.

  • @mqahnaf
    @mqahnaf 2 года назад

    love this ❤️ 3 years ago, I try to understand this the hard way by myself. But now I can simply recommend this video to my friends! Thanks Jago!

  • @antoniocortijo-rodgers75
    @antoniocortijo-rodgers75 Год назад

    I hope you’re all doin well
    - sorry had to say it

  • @tomholroyd7519
    @tomholroyd7519 2 года назад

    I suppose. But a statement can be valid without being satisfiable. Is there a thing like validity trees?

    • @AtticPhilosophy
      @AtticPhilosophy  2 года назад +2

      Any valid sentence is, by definition, satisfiable! Validity = has to be true, satisfiable = can be true.

  • @Someone-q6f5x
    @Someone-q6f5x 5 месяцев назад

    Just get to the point please🙏