Dear Joe,
Thanks for this fast reply.
This is what I got from running your command:
robert@keron:~/Project/holala.bit$ opentheory info --theory
--show-assumptions --show-derivations base
3 external type operators: -> bool ind
2 external constants: = select
3 assumptions:
(1) |- AXIOM OF EXTENSIONALITY
(2) |- AXIOM OF CHOICE
(3) |- AXIOM OF INFINITY
8 defined type operators: list option * + unit natural real set
148 defined constants: ! /\ ==> ? ?! \/ ~ cond F T :: @ [] all any
case.[].:: concat drop filter foldl foldr fromSet head interval last
length map member nth nub nubReverse null replicate reverse tail take
toSet unzip zip zipWith case.none.some isNone isSome map none some , fst
snd case.left.right destLeft destRight isLeft isRight left right () ^
const flip id injective o surjective Combinator.s Combinator.w * + - < <=
> >= ^ bit0 bit1 distance div even factorial isSuc log max min minimal
mod odd pre suc zero * + - / < <= > >= ^ ~ abs fromNatural inv max min
sup bigIntersect bigUnion empty fromSet intersect irreflexive measure
reflexive subrelation toSet transitive transitiveClosure union universe
wellFounded {} bigIntersect bigUnion bijections choice cross delete
difference disjoint finite fold fromPredicate hasSize image infinite
injections insert intersect member properSubset rest singleton size
subset surjections union universe
1,214 theorems:
|- T
{(1) (2) (3)}
|- null []
{(1) (2) (3)}
|- isNone none
{(1) (2) (3)}
|- even 0
{(1) (2)}
|- irreflexive empty
{(1) (2) (3)}
|- irreflexive isSuc
{(1) (2)}
|- reflexive universe
{(1) (2)}
|- transitive empty
{(1) (2)}
|- transitive universe
{(1) (2) (3)}
|- transitive (<)
{(1) (2)}
|- wellFounded empty
{(1) (2) (3)}
|- wellFounded (<)
{(1) (2) (3)}
|- wellFounded isSuc
...etc
I have the following questions:
1) It seems that the total amount of thms is different from my past
analysis, I had 1186 from the previous function you just pushed into
Opentheory but I got 1,214 theorems running this one. Have I missed
anything?
2) I am not familiar with AXIOM OF INFINITY, does it have anything to do
with identifying if a proof is classical or intuitionistic?
3) {(1) (2) (3)} means it is not 1, nor 2, nor 3 I guess?
Cheers
Robert
On 8 June 2015 at 19:47, Joe Leslie-Hurd <[email protected]> wrote:
> Hi Robert,
>
> It is easy to answer this question for the OpenTheory standard theory
> library by using this command:
>
> opentheory info --theory --show-assumptions --show-derivations base
>
> For each theorem this displays which of the three axioms
> (Extensionality, Choice and Infinity) it depends on.
>
> Cheers,
>
> Joe
>
> On Mon, Jun 8, 2015 at 10:40 AM, Robert White
> <[email protected]> wrote:
> > Dear all,
> >
> > I wonder how I can detect if there law of excluded middle or double
> negation
> > elimination used in a proof. Basically, I am trying to find out if a
> proof
> > is classical or constructive.
> >
> > Since when I use TAUT or other rewriting functions I won't get a direct
> idea
> > if it is classical or constructive. I wonder if there is anyway I can
> find
> > out.
> >
> > Thanks a lot.
> >
> > --
> >
> > Regards,
> > Robert White (Shuai Wang)
> > INRIA Deducteam
> > [Moving to ILLC of UvA from this Sep. ]
> > [New email address will be [email protected]]
> >
> >
> >
> ------------------------------------------------------------------------------
> >
> > _______________________________________________
> > hol-info mailing list
> > [email protected]
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >
>
--
Regards,
Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
[Moving to ILLC of UvA from this Sep. ]
[New email address will be [email protected]]
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
