6
$\begingroup$

Formally this is:

$\exists S [\forall \mathcal M (\mathcal (\mathcal M\models T) \to (\mathcal M \models S)) \wedge \neg (T \vdash S)]$

In English: there is a sentence in the language of an effectively generated theory $T$ that is satisfied in every model of $T$, and yet not provable in $T$.

Can this occur in some effective logical systems other than first order logic? What are those systems?

[EDIT]In first order logic systems this cannot happen because of Godel's completeness theorem for first order logic, which implies that satisfiability corresponds to syntactical provability, so if a sentence is satisfiable in every model of a first order theory, then it must be a provable in that theory.

$\endgroup$
15
  • 1
    $\begingroup$ You are perhaps aware, judging by your final paragraph, that this cannot happen in a finitely axiomatizable first-order theory (by Gödel's completeness theorem for the predicate calculus). It would be better to edit that into the body of the Question. $\endgroup$ Commented Apr 30, 2019 at 23:00
  • 3
    $\begingroup$ Just take first order logic and remove all axioms and rules of inference, so nothing is provable. Then the set of logical validities will work as an example. Or, take the first-order theory of Peano arithmetic, keep the usual inference rules, and throw out every every model except the standard one. Now Con(PA) is true in every model, but not provable. (This is very close to the situation with second-order PA.) . There are also intermediate options, for example use Heyting Arithmetic with the collection of classical models. Now the law of the excluded middle is valid but unprovable. $\endgroup$ Commented Apr 30, 2019 at 23:09
  • 1
    $\begingroup$ For users to write a more useful answer, it would help if you could add some additional context - what are you thinking about that led you to this question? Given the ease of generating examples, I'm afraid the XY effect (xyproblem.info) may be at play here. $\endgroup$ Commented Apr 30, 2019 at 23:18
  • 4
    $\begingroup$ @Zuhair - What do you mean by "effective theory"? The empty set, Peano arithmetic, and Heyting arithmetic are all effective theories / effectively generated theories in the usual meaning of the word - they have computable axiomatizations. The important point is that the definition of the logic itself determines both the deductive system and the collection of models - by changing either of those we can make syntactic provability differ from validity in all models. $\endgroup$ Commented May 1, 2019 at 11:50
  • 2
    $\begingroup$ I would say that a classical logical system, at the level of utmost generality, includes a set of sentences, a deductive consequence relation between sets of sentences, a collection of models, and a satisfaction relation between models and sentences. If you have a different definition of "logical system" in mind, could you clarify it in the question? Second-order logic with full semantics, in particular, is not essentially different than the second example I gave. $\endgroup$ Commented May 1, 2019 at 14:32

0

Reset to default

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.