0
$\begingroup$

Let's suppose classical propositional logic (model theory) and Hilbert's axiomatic system (proof theory). I know that in the Hilbert's axiomatic system there are inference rules for deriving new theorems from axioms. By those inference rules it is also possible to check afterwards whether the given formula follows from the axioms or theorems. On the other hand, I know that in classical propositional logic there is a rigorous way of checking whether a particular formula $A$ is a logical consequence of a theory $T$ (meaning set of formulas). By a rigorous way I mean checking based on the defined logical functions (meaning logical connectives) whether a formula $A$ is true in every possible truth assigment of formulas of a theory $T$. Although I'm not sure whether there is in the classical propositional logic some "recipe" as well for deriving logical consequences from the theory $T$. Or is it that in the model theory there are only "rules" for checking whether a given formula follows from the theory? If so, is this the fundamental difference between a proof theory and model theory?

I should note that I'm quite a beginner in this subject, so easy on me please.

$\endgroup$
  • 1
    $\begingroup$ "To generate" can be misleading... Prop logic in a nutshell: write a simple piece of code to produce all wff in some order (increasing length) and use truth table to check if it is a tautology. IT WORKS. FOL: write a simple piece of code to produce all wff in some order (increasing length) and use .... to check if it is valid. IT HAS BEEN PROVED THAT for FOL there is no mechanical procedure like truth-table to check validity. $\endgroup$ – Mauro ALLEGRANZA May 7 at 13:04
  • 1
    $\begingroup$ Thus, the answer to your "reformulated" question is: NO. There is no “recipe” for deriving logical consequences from given theory T in FOL. $\endgroup$ – Mauro ALLEGRANZA May 7 at 13:05
  • 1
    $\begingroup$ Not exactly; in general there is the proof system (the calculus) and interpretation (the semantics) for every logic. For propositional logic, the distinction is quite useless (see e.g. here). $\endgroup$ – Mauro ALLEGRANZA May 7 at 14:02
  • 1
    $\begingroup$ Model Theory "in a broader sense, is the study of the interpretation of any language, formal or natural, by means of set-theoretic structures." Due to the very very low complexity of the expressive capabilities of propositional logic, Model Th for prop logic is not very interesting. $\endgroup$ – Mauro ALLEGRANZA May 7 at 14:05
  • 1
    $\begingroup$ The goal of Proof Theory si "to understand the structure of mathematical proofs. Proof theory has created new aims outside traditional mathematics, especially in connection with computer science. Topics such as the verification of correctness of computer programs are an outgrowth of proof theory. Natural Deduction has led to the Curry-Howard correspondence and to connections with functional programming, and Sequent Calculus is often used in systems of automatic proof search, as in logic programming." $\endgroup$ – Mauro ALLEGRANZA May 7 at 14:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.