I am studying structural proof theory by Sara Negri, but I am having a problem, I can't understand what a principal formula is ? When she wants to prove a lemma or a theorem, she divides it into two conditions $(1)$When the formula is principal and $(2)$when its not. Whats the reason behind it ?
Asked
Active
Viewed 529 times
1 Answers
2
See page 15 :
The formula with the connective in a rule is the principal formula of that rule, and its components in the premisses are the active formulas. The Greek letters denote possible additional assumptions that are not active in a rule; they are called the contexts of the rules.
The principal fromula is the one "acted on" by the rule : reading the rule bottom-up, the principal formula is "decomposed" by the rule according to the corresponding connective, while the formulae in the context are left unchanged.
Mauro ALLEGRANZA
- 94,169
-
tnx.your answer was helpful.can you explain more about this sentence in page 32 please: "if A&B is not principal in the last rule,it has one OR two (???) premisses A&B,Γ′⇒C′ ,A&B,Γ′′⇒c″.....tnx alot – fateme jl Jan 16 '15 at 13:10
-
@fatima - the proof is by induction on the number $n$ of rules applied and the phrase is relative to the induction step. It is splitted into two case : i) A&B principal; ii) A&B not principal: this means that the said occurrence of A&B is in one of the contexts of the rule applied (which is not L&) and some rule (see page 28) has only one premise while some rule has two premsies. Because it is not principal (it occurs in a context) it is left unchanged by the applied rule in the original proof; thus, apply the induction hypo to them. – Mauro ALLEGRANZA Jan 16 '15 at 13:44
-
tnx alot for your helpful answer. – fateme jl Jan 16 '15 at 14:14