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 : it has the following axioms:
- A1.
- A2.
- A3.
we can substitute any propsitions inplace of with the connectives 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 be the set of premises (propositions), a proof sequence from is the sequence such that each statement in the sequence is one of 3 types:
- logical axiom
- a statement from
- is derived from previous statements in the sequence using one of the rules of inference of the system
premises: conclusion:
proof that is a tautology
an extended formal system axioms:
- such that is an arbitrary proposition
inference rules: the inference rules based on the logical equivalences and derivations that appear on the formulas page
prove premises: conclusion:
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 from the assumptions
- we can infer from
sometimes we might want to prove a conclusion with an empty set of premises: . an argument of this form is valid if is a tautology. meaning is a tautology iff we can prove that its always true without the need for assumptions: for example :
if then is a tautology, i.e. a proposition that can be formally proved without assumptions is a tautology
if then meaning that every proposition that has a formal proof in the set of premises logically follows from
a system is complete if for every set of assumptions , if then , i.e. we can formally prove every true argument with it
let be a set of assumptions, let be statements, then iff
let be a set of assumptions, let be statements, then iff