GoConqr has a new look! Let us know what you think.

Flashcards

Logic IV

kirsty.a.paton English 24 cards

Cards in this deck (24)

  1. 1SequentFinite set \(\Gamma\) of sentences on the lhs, the sumbol => in the middle and a finite set of sentences \(\Delta\) on the rhs
  2. 2DerivationAny finite sequence of sequents s.t. every sequent is either an assumption sequent or obtained from the previous sequent by the application of an inference rule
  3. 3D is deducible from \(\Gamma\)iff there's a derivation of \(\Gamma\) => D
  4. 4\(\Gamma\) is refutableiff there's a derivation of \(\Gamma\) => \(\psi\)
  5. 5D is deducibleiff there's a derivation of \(\psi\) => {D}
  6. 6A set \(\Gamma\) secures a set \(\Delta\)if every interpretation that makes all sentence in \(\Gamma\) true makes some sentence in \(\Delta\) true
  7. 7D is a consequence of \(\Gamma\)iff \(\Gamma\) secures {D}
  8. 8\(\Gamma\) is unsatisfiableiff \(\Gamma\) secures \(\psi\)
  9. 9D is validiff \(\psi\) secures {D}
  10. 10R0\(\overline{A => A}\)
  11. 11k\(\Gamma\) => \(\Delta\)/\(\Gamma'\) => \(\Delta'\)
  12. 12~R\(\Gamma\),A => A/ \(\Gamma\) => ~A,\(\Delta\)
  13. 13~L\(\Gamma\) => A,\(\Delta\) / \(\Gamma\),~A => \(\Delta\)
  14. 14vR\(\Gamma\) => A,B,\(\Delta\) / \(\Gamma\) => A v B, \(\Delta\)
  15. 15v L\(\Gamma\),A => \(\Delta\) \(\Gamma\),B => \(\Delta\) / \(\Gamma\),A v B => \(\Delta\)
  16. 16\(\exists\)L\(\Gamma\),A[s/x] =>\(\Delta\) / \(\Gamma\),\(\exists\)xA => \(\Delta\)
  17. 17\(\exists\)R\(\Gamma\) =>A[s/x],\(\Delta\) / \(\Gamma\) => \(\exists\)xA,\(\Delta\)
  18. 18R7\(\Gamma\),s=s => \(\Delta\) / \(\Gamma\) => \(\Delta\)
  19. 19=L1\(\Gamma\) => A(t),\(\Delta\) / \(\Gamma\), s=t => A(s),\(\Delta\)
  20. 20=L2\(\Gamma\),A(t) => \(\Delta\) / \(\Gamma\),s = t, A(s) =>\(\Delta\)
  21. 21A proof system is sound relative to semanticswhenever every proof corresponds to a valid inference
  22. 22A proof system is complete relative to semanticsif every valid inference corresponds to a proof
  23. 23Soundness TheoremEvery derivable sequent is secure
  24. 24Completeness TheoremEvery secure sequent is derivable

Information

Description
Genzen Squent Calculus, Soundness and Completness
Created by
kirsty.a.paton · May 2014
Updated
Feb 19, 2016
Views
27
Rating

Feedback

What is it about?

What do you think of the new look?

How do you like it?