formal system

a formal system is an abstract structure used for inferring theorems from axiom according to a set of rules of inference which are used for carrying out the inference of theorems from axioms.

consider the following formal system $\text{[math]}$ :
it has the following axioms:

A1. $\text{[math]}$
A2. $\text{[math]}$
A3. $\text{[math]}$

we can substitute any propsitions inplace of $\text{[math]}$ with the connectives $\text{[math]}$ only
the only rule of inference for this system is mp

the inference process in the context of a formal system is as follows:
let $\text{[math]}$ be the set of premises (propositions), a proof sequence from $\text{[math]}$ is the sequence $\text{[math]}$ such that each statement in the sequence is one of 3 types:

logical axiom
a statement from $\text{[math]}$
is derived from previous statements in the sequence using one of the rules of inference of the system

premises: $\text{[math]}$
conclusion: $\text{[math]}$

$\text{[math]}$

proof that $\text{[math]}$ is a tautology

$\text{[math]}$

an extended formal system $\text{[math]}$
axioms:

$\text{[math]}$ such that $\text{[math]}$ is an arbitrary proposition

inference rules: the inference rules based on the logical equivalences and derivations that appear on the formulas page

prove $\text{[math]}$
premises: $\text{[math]}$
conclusion: $\text{[math]}$

$\text{[math]}$

prove using the inference process that

we can infer "joseph doesnt speak truthfully" from the assumptions "joseph doesnt speak truthfully or joseph is lazy" and "joseph isnt lazy"
we can infer $\text{[math]}$ from the assumptions $\text{[math]}$
we can infer $\text{[math]}$ from $\text{[math]}$

sometimes we might want to prove a conclusion $\text{[math]}$ with an empty set of premises: $\text{[math]}$ . an argument of this form is valid if $\text{[math]}$ is a tautology. meaning $\text{[math]}$ is a tautology iff we can prove that its always true without the need for assumptions: for example $\text{[math]}$ : $\text{[math]}$

if $\text{[math]}$ then $\text{[math]}$ is a tautology, i.e. a proposition that can be formally proved without assumptions is a tautology

if $\text{[math]}$ then $\text{[math]}$
meaning that every proposition that has a formal proof in the set of premises $\text{[math]}$ logically follows from $\text{[math]}$

a system is complete if for every set of assumptions $\text{[math]}$ , if $\text{[math]}$ then $\text{[math]}$ , i.e. we can formally prove every true argument with it

$\text{[math]}$

let $\text{[math]}$ be a set of assumptions, let $\text{[math]}$ be statements, then $\text{[math]}$ iff $\text{[math]}$