Is there any proof system with classical semantic that can drive all sentences but tautology?

35 Views Asked by At

In propositional calculus(sentencial logic) or predicate calculus(predicate logic), there is a typical semantic for giving True of False for their sentences. I will keep this semantic.

And there are so many proof systems which satisfy soundness and completeness. (e.g. Hilbert system with various axioms and Modus Ponens, or Natural deduction system, and so on. If the expressive power of connectives is enough, then every connective doesn't have to be used. And there should be infinitely many sentences in the system.)

And I will define some concepts.

Let A be the set of sentences, p be the sentence.

Anti-semantic : if p can be derived by A, then AU{p} isn't satisfiable or p is in A.

Anti-completeness : if AU{p} isn't satisfiable, then p can be derived by A.

(In this text, that A is satisfiable means that there is a truth-value assignment where all sentences of A is true.)

Is there a proof system that satisfies both anti-semantic and anti-completenss?

(Actually, if derivative rule can be freely changed, then there is such a system. For a given set A, we can think A' as all the formulas that can be derived from A in some system with completeness and soundness. And just let any formula be able to be derived from A if it isn't a member of A'. But I think it's not constructive proof system. If we want to derive some sentence in that such system, we should know semantic and check it or other proof system and make A'. So I hope that the derivative rule just reference the sentence of A or other sentences already derived.)