Logiweb codex of logic in pyk

Up Help

ref-0-id-0	logic
ref-0-id-1	double rule prime mp
ref-0-id-2	inference axiom prime a one
ref-0-id-3	rule hypothesize
ref-0-id-4	inference axiom prime a two
ref-0-id-5	inference inference axiom prime a two
ref-0-id-6	hypothetical rule prime mp
ref-0-id-7	double inference inference axiom prime a two
ref-0-id-8	double hypothetical rule prime mp
ref-0-id-9	mendelson lemma one eight
ref-0-id-10	inference mendelson lemma one eight
ref-0-id-11	rule repetition
ref-0-id-12	mendelson exercise one fourtyseven b
ref-0-id-13	mendelson exercise one fourtyseven c
ref-0-id-14	mendelson exercise one fourtyseven e
ref-0-id-15	mendelson lemma one eleven d
ref-0-id-16	hypothetical inference axiom prime a one
ref-0-id-17	hypothetical inference axiom prime a two
ref-0-id-18	hypothetical inference inference axiom prime a two
ref-0-id-19	hypothetical mendelson exercise one fourtyseven b
ref-0-id-20	hypothetical mendelson exercise one fourtyseven c
ref-0-id-21	mendelson lemma one eleven c
ref-0-id-22	mendelson exercise one fourtyeight d
ref-0-id-23	mendelson exercise one fourtyeight e
ref-0-id-24	mendelson exercise one fourtyeight h
ref-0-id-25	mendelson corollary one ten a
ref-0-id-26	mendelson corollary one ten b
ref-0-id-27	inference axiom prime s one
ref-0-id-28	inference inference axiom prime s one
ref-0-id-29	inference axiom prime s two
ref-0-id-30	hypothetical inference axiom prime s two
ref-0-id-31	inference inference axiom prime s nine
ref-0-id-32	rule induction
ref-0-id-33	mendelson proposition three two a
ref-0-id-34	mendelson proposition three two b
ref-0-id-35	inference mendelson proposition three two b
ref-0-id-36	mendelson proposition three two c
ref-0-id-37	inference inference mendelson proposition three two c
ref-0-id-38	hypothetical inference inference mendelson proposition three two c
ref-0-id-39	mendelson proposition three two d
ref-0-id-40	inference inference mendelson proposition three two d
ref-0-id-41	hypothetical inference inference mendelson proposition three two d
ref-0-id-42	mendelson proposition three two f
ref-0-id-43	mendelson proposition three two f i
ref-0-id-44	mendelson proposition three two f ii
ref-0-id-45	mendelson proposition three two g
ref-0-id-46	mendelson proposition three two g i
ref-0-id-47	mendelson proposition three two g ii
ref-0-id-48	mendelson proposition three two h
ref-0-id-49	mendelson proposition three two h i
ref-0-id-50	mendelson proposition three two h ii
ref-0-id-51	hypothesis
ref-0-id-52	instance
ref-0-id-53	conclusion
ref-0-id-54	* macro modus ponens *
ref-0-id-55	* macro first modus ponens * macro second modus ponens *
ref-0-id-56	* hypothetical macro modus ponens *
ref-0-id-57	* hypothetical macro first modus ponens * hypothetical macro second modus ponens var *
ref-0-id-58	line * hypothesis modus ponens * modus ponens * indeed * end line *
ref-0-id-59	line * hypothesis first modus ponens * modus ponens * indeed * end line *
ref-0-id-60	line * hypothesis second modus ponens * modus ponens * indeed * end line *
ref-0-id-61	line * hypothesis double modus ponens * modus ponens * modus ponens * indeed * end line *
ref-0-id-62	line * hypothesis indeed * end line *
ref-0-id-63	line * hypothesis because * indeed * end line *
ref-0-id-64	line * hypothesis raw because * indeed * end line *