PC(1): An introductory formal logic

For the past few years, I have been toying with the idea of an
elementary formal logic, to introduce formal systems to school-age and
even pre-school children. I'd like to put my most recent effort, which
I've called PC(1), on the group for review.

As well as general comments, I would be interested in any problems of
the system, from the name to the inferences to typos, being brought to
my attention.

--------------------------------------


I. PC(1)

Vocabulary

PC(1) is a language containing:
one proposition, P.
two grouping indicators, ( and ).
three operators, ~, &, and v.


Grammar.
1. Only well-formed formulas of PC ('wff') are allowed in PC(1).
2. A means any wff.
2. P is a wff.
3. ~P, ~~P, ~~~P, and ~~~~P are wff.
4. If A is a wff, then ~(A) is a wff.
5. If A is a wff, then (A & A) is a wff.
6. If A is a wff, then (A v A) is a wff.


Definitions

I.i Define |- as:
For any wff A and B,
A |- B iff "A, therefore B" is a valid inference in PC(1).

I.ii Define ~ as:
For any wff A, A is True iff ~A is false.

I.iii Define & as:
For any wff A, A is True iff (A & A) is true.

I.iv Define v as:
For any wff A,
A is True iff (A v A) is true.


Truth Tables

I.A A ~A
n T F I.ii
m F T I.ii

1B. A (A & A)
n T T I.ii
m F F I.ii

1C. A (A v A)
n T T
m F F


Inferences:
I.1 A |- ~~A
I.2 ~~A |- A

Proof:
1D. A ~A ~~A
n T F T I.A, n
m F T F I.A, m

I.3 A |- A & A
I.4 A & A |- A
Proof : see table 1B.

I.5 A |- A v A
I.6 A v A |- A
Proof: see table 1C.

.

Relevant Pages

  • Re: PC(1): An introductory formal logic
    ... the system, from the name to the inferences to typos, being brought to ... ignoring the question of why we want to confuse the kids ... definition of "wff", in which case you need to say so. ... A is True iff is true. ...
    (sci.logic)
  • Re: PC(1): An introductory formal logic
    ... For any wff A and B, ... A |- B iff "A, therefore B" is a valid inference in PC. ... A is True iff is true. ... An axiom is a formula that is true in every interpretation. ...
    (sci.logic)
  • Re: PC(1): An introductory formal logic
    ... It can't be to better understand ordinary reasoning, ... definition of "wff", in which case you need to say so. ... A is True iff is true. ... kids a formal system that can deduce P&P from P, ...
    (sci.logic)