Semi Substitivity

Introduction

Terminology aside: The original term, as coined by Zeman, is "Semisubstitutivity". I can neither reliably pronounce, nor reliably type this. So hopefully people won't object too strongly if I use the (easier for me) term "Semi-substitivity"

I'm sure that most readers of this are familiar with the concept in many logics of "substitution of equivalences". It says (roughly) that if you have p implying q, and q implying p, then you may substitute one for the other anywhere.

It is natural, for people with the right world view, to ask the question: "If p implying q, and q implying p, license replacing one for the other anywhere in an expression, is there something that JUST p implying q licenses you to do?" The short answer is yes, and the long answer is that deep into an expression there are places where you may replace p by q if you find a p. And even more surprising, all the other positions in the expression where you have no license to replace p by q, you DO have license to replace q by p if q is found.

While all positions in an expression tree that are in the scope of only implicational operators obeying semi-substitivity license the substitution one way or the other, which way is allowed at each position is somewhat awkward to state, and is done below with the proof.

If we have a substitution instance of p > q (Call it p' > q') then you can replace p' by q' anywhere you can replace p by q. And q' can be replaced by p' anywhere q can be replaced by p. This allows some local substitutions to be done without having to do the substitution uniformly into the entire expression. (Substitute into (p>q) and then proceed with semi-substitivity.)

History

To the best of my knowledge, the term "Semisubstitutivity" was coined by the logician J. Jay Zeman in his paper "A system of Implicit Quantification" in the Journal of Symbolic Logic, Volume 32 (1967) pages 480-504, where it was introduced and played a somewhat minor role.

The concept achieved star billing the next year in his paper "The Semisubstitutivity of Strict Implication", J. Jay. Zeman, Journal of Symbolic Logic, Volume 33 # 3 (1968). He mentions (but doesn't prove) that it is true in standard PC, intuitionistic PC, and other logics, and explicitly constructs it for a series of modal logics. The construction leans on the details of implication in the systems in question, and parts of the discussion depended on "counting the negations" when the implication was reduced to the modal operators, negation, and "or". In my opinion this contributed to people thinking of it in those terms, and not doing much with it in any more general context.

These papers did not attract much attention. For example, to the best of my my knowledge, the second paper didn't have a single paper reference it in the 40+ years since it came out.

Unknown to me when I started this page, the idea was independently discovered by Anderson and Belnap and appears in volume 1 of their book "Entailment" published in 1975. Judging by the Bibliography, they were unaware of Zeman's work on the topc. They refer to it as the Replacement Theorem.

Also unknown to me when I started this page, related ideas were independently developed by Zohar Manna and Richard Waldinger who pursued the ideas in an automated theorem proving context. "Special Relations in Automated Deduction" [Journal of the ACM (JACM), Volume 33, Issue 1, (January 1986) pages 1-59]. Note that they use the term "substitutivity". I assume that they were independent because their bibliography lists neither the Zeman works, nor Anderson and Belnap's book. They call their version Relation Replacement.

Actual proofs

Proofs of substitution of equivalents often proceed from showing that if a location in an expression is within the scope of only implications then the substitutions can be done, to showing it is still true as you introduce other operators.

This page will prove at locations in an expression that are in the scope of any implicational operators in the system that have certain common properties. Other operators can generally (but tediously) be shown to extend the properties to their scope directly from the axioms that define them and the proof for the implicational operator(s) of the system.

Assumptions

If you have uniform substitution, and you have one or more implicational operators that obey the rule of Modus Ponens, and you have for each of them the theorems or axioms of:

Then, by the proof given below, you have semi-substitivity for any location in an expression that is in the scope of JUST those implicational operators.

Comments

Below we prove the theorems for the rules of semi-substitivity, and because we have Modus Ponens, we therefore have the rules as well as the theorems. The system MUST have modus ponens. There are "Equivalent" systems with exactly the same theorems, but with rules weaker than modus ponens (such as Jean Porte's version of PC in the 1960's and Lloyd Humberstone's systems recently) that don't give us the rules from the theorems since they are too weak to prove the rule of modus ponens.

Given p implies q, stating where p can be replaced by q (let's call this forward replacement) and where q can be replaced by p (let's call this reverse replacement) is somewhat awkward. As we look at the expression tree, the top level node (by modus ponens) allows forward replacement. As we go down the consequent (right) branch of a node the node below inherits the direction of the parent. As we go down the antecedent (left) branch the node has the opposite direction to its parent.

For polish notation in expressions with just the implicational operators there is a very simple labeling of forward and reverse. The first operator has forward replacement, the next token has reverse replacement, and it alternates token wise down the string. [Token wise since multicharacter variable names (like v12) need to be treated as a single item]. (To the best of my knowledge, while I rediscovered it, the first place of publication appears to be Anderson and Belnap's "Entailment" where it is attributed to John Bacon.

As an example, let's take the expression (p > q) > (r > s) and mark where each flavor of replacement can be done. (Using + for forward replacement and - for reverse replacement.


Infix:
(p > q) > (r > s)
 + - -  +  - + + 
 
Polish:
CCpqCrs
+-+-+-+

Modus Ponens is semi-substitivity at top level, B and B' are semi-substitivity at the next level down, and theorems 3 had 5 extend semi-substitivity down one level from whatever level we have already proven. So by induction we can build the semi-substitivity rules to cover any finite expression in the implicational operators meeting the assumptions.

Actually, only the first eight lines of the proof are strictly needed, but I generated the next level for those people that are more comfortable with more examples.

Machine generated part of proof

Convert to infix Notation

Expand out condensed detachment steps


# ----------------- Proof: --------------------
# Produced Wed Jul  7 10:31:17 2010
# by the "shotgun" program, version 2010-01-07 0.01.007
# Axiomatic Basis:
      =basis     B
          =basis B'

#    --  Rules --

#  Condensed detachment for C 
#      From |- p and |- Cpq,  produce the most general possible |- q.
#
#          --- Wish List ---

      =wishlist "CCpqCCqrCpr"         "Semi A (Antecedent)"
      =wishlist "CCpqCCrpCrq"         "Semi C (Consequent)"
      =wishlist "CCpqCCCprsCCqrs"     "Semi AA (Antecedent of Antecedent)"
      =wishlist "CCpqCCCrqsCCrps"     "Semi CA (Consequent of Antecedent)"
      =wishlist "CCpqCCrCqsCrCps"     "Semi AC (Antecedent of Consequent)"
      =wishlist "CCpqCCrCspCrCsq"     "Semi CC (Consequent of Consequent)"
      =wishlist "CCpqCCCCqrstCCCprst" "Semi AAA"
      =wishlist "CCpqCCCCrpstCCCrqst" "Semi CAA"
      =wishlist "CCpqCCCrCpstCCrCqst" "Semi ACA"
      =wishlist "CCpqCCCrCsqtCCrCspt" "Semi CCA"
      =wishlist "CCpqCCrCCpstCrCCqst" "Semi AAC"
      =wishlist "CCpqCCrCCsqtCrCCspt" "Semi CAC"
      =wishlist "CCpqCCrCsCqtCrCsCpt" "Semi ACC"
      =wishlist "CCpqCCrCsCtpCrCsCtq" "Semi ACC"

#          --- Axioms ---
=axiom "CCpqCCrpCrq" "B"

# Wish list theorem: Semi C (Consequent)
 1: CCpqCCrpCrq                              # B
=axiom "CCpqCCqrCpr" "B'"

# Wish list theorem: Semi A (Antecedent)
 2: CCpqCCqrCpr                              # B'

=lastaxiom

#          --- Theorems ---

 3: CCpCqrCpCCsqCsr                          # Condensed detachment, inference line 1 with line 1
                                             #   proof: D 1 1 cost=1

# Wish list theorem: Semi AC (Antecedent of Consequent)
 4: CCpqCCrCqsCrCps                          # Condensed detachment, inference line 3 with line 2
                                             #   proof: D D 1 1 2 cost=2

 5: CCpCqrCpCCrsCqs                          # Condensed detachment, inference line 1 with line 2
                                             #   proof: D 1 2 cost=1

# Wish list theorem: Semi CA (Consequent of Antecedent)
 6: CCpqCCCrqsCCrps                          # Condensed detachment, inference line 5 with line 1
                                             #   proof: D D 1 2 1 cost=2

# Wish list theorem: Semi AA (Antecedent of Antecedent)
 7: CCpqCCCprsCCqrs                          # Condensed detachment, inference line 5 with line 2
                                             #   proof: D D 1 2 2 cost=2

# Wish list theorem: Semi CC (Consequent of Consequent)
 8: CCpqCCrCspCrCsq                          # Condensed detachment, inference line 3 with line 1
                                             #   proof: D D 1 1 1 cost=2

# Wish list theorem: Semi ACC
 9: CCpqCCrCsCqtCrCsCpt                      # Condensed detachment, inference line 3 with line 4
                                             #   proof: D D 1 1 D D 1 1 2 cost=3

# Wish list theorem: Semi CAA
10: CCpqCCCCrpstCCCrqst                      # Condensed detachment, inference line 5 with line 6
                                             #   proof: D D 1 2 D D 1 2 1 cost=3

# Wish list theorem: Semi AAA
11: CCpqCCCCqrstCCCprst                      # Condensed detachment, inference line 5 with line 7
                                             #   proof: D D 1 2 D D 1 2 2 cost=3

# Wish list theorem: Semi ACC
12: CCpqCCrCsCtpCrCsCtq                      # Condensed detachment, inference line 3 with line 8
                                             #   proof: D D 1 1 D D 1 1 1 cost=3

# Wish list theorem: Semi AAC
13: CCpqCCrCCpstCrCCqst                      # Condensed detachment, inference line 3 with line 7
                                             #   proof: D D 1 1 D D 1 2 2 cost=4

# Wish list theorem: Semi CAC
14: CCpqCCrCCsqtCrCCspt                      # Condensed detachment, inference line 3 with line 6
                                             #   proof: D D 1 1 D D 1 2 1 cost=4

# Wish list theorem: Semi CCA
15: CCpqCCCrCsqtCCrCspt                      # Condensed detachment, inference line 5 with line 8
                                             #   proof: D D 1 2 D D 1 1 1 cost=4

# Wish list theorem: Semi ACA
16: CCpqCCCrCpstCCrCqst                      # Condensed detachment, inference line 5 with line 4
                                             #   proof: D D 1 2 D D 1 1 2 cost=4

# Final proof had 16 lines (14 steps)
# ------------------ End proof --------------

Go to ...


This page is http://www.cc.utah.edu/~nahaj/logic/concepts/semi/index.polish.html
© Copyright 2010 by John Halleck, All Rights Reserved.
This page was last modified on August 11th, 2010