Antimatroids were discovered by Dilworth in the context of lattices  and introduced by Edelman and Jamison as convex geometries in. The author of the current paper independently discovered (possibly infinite) antimatroids in the context of proof systems in mathematical logic . Carlson, a logician, makes implicit use of this view of proof systems as possibly infinite antimatroids in . Though antimatroids are in a sense dual to matroids, far fewer antimatroid forbidden minor theorems are known. Some results of this form are proved in , , , and . This paper proves two forbidden induced minor theorems for these objects, which we think of as proof systems. Our first main theorem gives a new proof of the forbidden induced minor characterization of partial orders as proof systems, proved in  in the finite case and stated in  for what we call strong aut descendable proof systems. It essentially states that, pathologies aside, there is a certain unique simplest nonposet. Our second main theorem states the new result that, pathologies aside, there is a certain unique simplest proof system containing points $x$ and $y$ such that $x$ needs $y$ in one context, yet $y$ needs $x$ in another.