Axiom Schemas for Andrews' System F for first order logic (not to be confused with Girard's System F for polymorphic lambda calculus). Keep in mind disjunction, negation and universal quantifiers are the only primitives. The other connectives are abbreviations.

Axiom Schema 1. A or A implies A

Axiom Schema 2. A implies . B or A

Axiom Schema 3. A implies B implies . C or A implies . B or C

Axiom Schema 4. forall x A implies S^x_t A; assuming t is free for x in A.

Axiom Schema 5. forall x [A or B] implies . A or forall x B; assuming x is not free in A.

Rules of Inference:

Modus Ponens. From A and not A or B we can infer B.

Generalization. From A we can infer forall x A.