0
$\begingroup$

In a logic system, a formula which holds under all interpretations is called a tautology (e.g. in propositional logic) or valid formula (e.g. in FOL).

Is there a name for a formula $\phi$ which satisfies $\vdash \phi$? (I don't expect it to be called a tautology or valid formula again, because I don't assume completeness and soundness.)

Is it correct that $\vdash \phi$ means that $\phi$ is derivable from a specific set of axioms?

Does the concept of "axiom" make sense only with respect to a specific proof system? Or is it a concept independent of specific proof systems?

Does $\vdash \phi$ make sense only with respect to a specific proof system? More specifically, does $\vdash \phi$ make sense only with respect to the set of axioms in a specific proof system?

Thanks.

$\endgroup$
1
  • 1
    $\begingroup$ "Is it correct that ⊢ϕ means that ϕ is derivable from a specific set of axioms?" Yes. It's called a theorem. "Does the concept of "axiom" make sense only with respect to a specific proof system?" Only with respect to a proof system. "Does ⊢ϕ make sense only with respect to a specific proof system? More specifically, does ⊢ϕ make sense only with respect to the set of axioms in a specific proof system?" Yes. $\endgroup$ – Doug Spoonwood Sep 13 '20 at 23:30
2
$\begingroup$

Is there a name for a formula $\phi$ which satisfies $\vdash \phi$? (I don't assume completeness and soundness.)

Yes. It is called a theorem.

Is it correct that $\vdash \phi$ means that $\phi$ is derivable from a set of axioms?

Depends on the proof system/theory. If it has axioms, then yes, it is derivable from a set of axioms plus inference rules; if the proof system has only rules of inference, then it just means derivable from the inference rules.

Does the concept of "axiom" make sense only with respect to a specific proof system? Or is it a concept independent of specific proof systems?

Both.
On the one hand, when talking about the general laws of predicate logic that hold universally in all structures, there are some proof systems which have axioms and others which don't.
On the other hand, one often deals with derivability in a theory, such as Peano arithmetic or ZF(C) set theory, which talk about a spefific mathematical domain (such as the natural numbers, or sets) and prove additional theorems about this subject. Such theories are obtained by adding theory-specific axioms on top of the existing proof system for the basic logical laws. Then one can also incorporate axioms in a proof system like Natural Deduction, which doesn't have axioms by default, by allowing to introduce axioms as assumptions in a derivation at any time, without having to write them down to the left-hand side of the $\vdash$ symbol every time anew, if the context makes it clear that $\vdash$ means derivability in this particular theory with the addition of axioms.

Does $\vdash \phi$ make sense only with respect to a specific proof system? More specifically, does $\vdash \phi$ make sense only with respect to the set of axioms in a specific proof system?

Yes. When writing $\vdash$, you always have a specific proof system in mind. Again, considering axioms only makes sense if the proof system actually has axioms.

$\endgroup$
2
  • $\begingroup$ Thanks. Given a language (e.g. first order language), are different proof systems not required to induce the same derivability relation $\vdash$ between sets of formulas and formulas? $\endgroup$ – Tim Sep 13 '20 at 23:41
  • $\begingroup$ Each proof system potentially produces its own derivability relation, and one has one particular proof system in mind when talking about $\vdash$. But in many cases, different proof system will in fact eventually turn out to be equivalent in terms of the relation they induce. Is that what you mean? $\endgroup$ – lemontree Sep 14 '20 at 0:44

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.