Can dummy True/False be in the consequent side of the implication and what it could mean?

Question

It is known that False -> SomeFact is the use of the implication for the representation of the facts in the propositional and first order logic. The Sequent (of the sequence calculus) is the implication whose antecedant is some conjunction of formulas and whose consequent is some disjunction of formulas. The sequent format requires that something should be in the antecedant and in the consequent (those sets of formulas can not be empty - as I understand) and my question is: can True exclusively-or False be the only members of the consequent of the implication and what such implications mean?

My question is connected to my other question: https://cs.stackexchange.com/questions/118588/can-full-first-order-knowledge-base-be-written-as-the-single-sequent-in-the-sequ which asks whether single sequent can represent entire knowledge base? Knowledga base, as we know, is the set for formulas, i.e. the long conjunction of the formulas, can any such conjunction be converted to the implication, i.e. to the sequent?

Answer 1

In the usual presentation of sequent calculus [see e.g. Gaisi Takeuti, Proof Theory (1987), page 8] :

$\Gamma, \Delta$ denote finite (possibly empty) sequences of formulas [...].

Def.1.8 For arbitrary $\Gamma$ and $\Delta$ in the above notation, $\Gamma \to \Delta$ is called a sequent.

A sequent of the form $A \to A$ is called an initial sequent or axiom.

If we have the $\bot$ symbol in the language, the following sequent is an axiom : $\bot \to \bot$.

Thus, using $\supset \text {-right}$ [I'll use $\supset$ for the conditional, having used $\to$ for the sequent] we immediately conclude with :

$\to \bot \supset \bot$

that can be read as $\to \lnot \bot$, i.e. as $\to \top$.

What is the meaning of the sequent : $\to \bot$ ?

We have that [see page 11] a formula $\varphi$ is provable (in the calculus) if the sequent $\to \varphi$ is provable. From the semantical point of view, by soundness, this means that $\varphi$ is a valid formula.

Thus, to derive the sequent $\to \bot$ amounts to a proof that the calculus is inconsistent.

---

If the logic does not include $\bot$, we have that [see page 9] the empty sequent $\to$ means that there is a contradiction.

Thus, the definition of inconsistent is the following [see page 21] :

A system $\mathscr A$ [a finite or infinite set of sentences, called the axioms of the system, that means adding to the calculus the initial sequents : $\to A$, for every $A$ in $\mathscr A$] is inconsistent if the empty sequent : $\to$ is provable from $\mathscr A$.

---

---

As discussed in some previous thread, the "application" of sequent calculus to some "topic" needs an initial set of non-logical axioms : specific mathematical axioms for e.g. a mathematical theory or specific "facts" related to a knowledge base.

These axioms must be expressed as initial sequents of the form $\to \text {Ax}$.