[Axiom-developer] [15-819] Proofs as math objects

[Tim Daly]

I'm a computational mathematician (CM) so I'm coming to the logic

area from left field (deep left, out by the fence). Thus my question

might not make sense.

You made the passing comment that proofs are mathematical

objects like numbers.

What I HEARD was... proofs are like Integers. To a CM that means

(a) there are a set of functions that operate on Integers and

(b) Integers are opaque.

For instance, in Axiom, Integers are:

(1) -> )show Integer
Integer is a domain constructor
Abbreviation for Integer is INT
This constructor is exposed in this frame.
Issue )edit bookvol10.3.pamphlet to see algebra source code for INT ------------------------------- Operations --------------------------------
?*? : (%,%) -> %
?*? : (Integer,%) -> %
?*? : (PositiveInteger,%) -> %
?**? : (%,PositiveInteger) -> %
?+? : (%,%) -> %
?-? : (%,%) -> %
-? : % -> %
?<? : (%,%) -> Boolean
?<=? : (%,%) -> Boolean
?=? : (%,%) -> Boolean
?>? : (%,%) -> Boolean
?>=? : (%,%) -> Boolean
D : % -> %
D : (%,NonNegativeInteger) -> %
OMwrite : (%,Boolean) -> String
OMwrite : % -> String
1 : () -> %
0 : () -> %
?^? : (%,PositiveInteger) -> %
abs : % -> %
addmod : (%,%,%) -> %
associates? : (%,%) -> Boolean
base : () -> %
binomial : (%,%) -> %
bit? : (%,%) -> Boolean
coerce : Integer -> %
coerce : % -> %
coerce : Integer -> %
coerce : % -> OutputForm
convert : % -> String
convert : % -> DoubleFloat
convert : % -> Float
convert : % -> Pattern(Integer)
convert : % -> InputForm
convert : % -> Integer
copy : % -> %
dec : % -> %
differentiate : % -> %
even? : % -> Boolean
factor : % -> Factored(%)
factorial : % -> %
gcd : List(%) -> %
gcd : (%,%) -> %
hash : % -> %
hash : % -> SingleInteger
inc : % -> %

      ..... etc.

But that seems odd to me, in two ways. First, Proofs seem more like

Polynomials. Polynomials don't have any meaning until you specify the

base ring, e.g. Polynomial(Integer) or Polynomial(Fraction(Integer)).

Once you give me the base ring I know what operations I can perform.

Proofs seem to need the set of sequents and the set of hypotheses in

order to be concrete, e.g. Proof(Heyting,LEM). Without specifying these

constraints I have no idea what a "Proof" means computationally. You

might also have to specify further information (ala Lakatos).

Second, Proofs, like Polynomials, have "internal structure". You can ask a

Polynomial for its leading coefficient. Similarly, you could ask a Proof for

one of its goals. You can write tactics that manipulate the internal structure

of a Proof object (like you can manipulate terms in a Polynomial).

But my question is, given a Proof object as a "mathematical object"

what possible operations can be performed on a proof as an "opaque"

object? Does it make sense to "multiply" proofs? Clearly you can "'and"

them together but I don't know how useful that operation would be.

At most, I might have a "refute" operation but nothing else leaps to mind.

Tim, the confused CM.