Derivation and Hypothesis in First order Logic

Question

Studying First Order logic , i found for the first time the term "Hyphotesis" when the my book introduced the derivation of a sentence from a Formal System and a a set S of hyphotesis and assumptions.

My questions is: why in first order logic hypothesis cant be open sentences ?

Answer 1

Why not?

See a typical definition (Enderton, page 110):

We will shortly select an infinite set $\Lambda$ of formulas to be called logical axioms. And we will have a rule of inference, which will enable us to obtain a new formula from certain others. Then for a set $\Gamma$ of formulas [emphasis added], the theorems of $\Gamma$ will be the formulas which can be obtained from $\Gamma \cup \Lambda$ by use of the rule of inference (some finite number of times).

If $\varphi$ is a theorem of $\Gamma$ (written $\Gamma \vdash \varphi$), then a sequence of formulas that records (as explained below) how $\varphi$ was obtained from $\Gamma \cup \Lambda$ with the rule of inference will be called a deduction of $\varphi$ from $\Gamma$.

---

There are some restrictions involving open formulas regarding the Deduction Th in the Hilbert-style presentation of the calculus, or in the rules of $\forall$-intro ("geenralization") in Natural Deduction.

Answer 2

The consequence relation itself doesn't prohibit free variables. For example the LK calculus by Gentzen is based on sequents of the form:

G |- D

Were G and D are lists of formulas, and these formulas need not be closed. In LK the deduction theorem even doesn't need any provisio, since there is an inference rule "right implication introduction" (called FES by Gentzen):

G, A |- B
----------- (=> R)
G |- A => B

Nevertheless there is often a tacit assumption that axioms are universally closed, so that axioms do not occupy some variable names.

But when closed axioms are used, this doesn't mean that in the course of a proof no open formulas might appear. A typical inference rule that breaks axioms open, in LK, is the "left forall introduction" rule (called AEA by Gentzen):

G, A[x/t] |- B
------------------- (forall L)
G, forall x A |- B