This is a submission for the Special Issue on Neurosymbolic AI: First-Order Logic and Beyond. It contains an exploration of the diverse interpretation of inconsistent assumptions taken from elementary probability across LLMs and proof checkers and then a first order axiomatization that, at least theoretically, guarantees consistency. In particular, the manuscript combines two closely connected contributions: a controlled benchmark of inconsistent-premise reasoning in LLM and proof-assistant workflows, and a first-order semantic and a Lean implementation framework for premise-consistency checking in finite probability. I consider potential inconsistencies a relevant issue as more automated proofs are being developed in a direct interaction between LLMs and proof assistants. I have retained the the two parts in one manuscript because the empirical study identifies the assurance gap, while the formal theory and ProbConsistency implementation explain and address it. The manuscript nevertheless has a natural division between the benchmark study and the first-order system contribution. Should the editors consider the benchmark component better suited to the journal’s separate Special Call for Neurosymbolic Benchmark Papers, I would welcome guidance on an internal transfer or on preparing two clearly differentiated companion manuscripts. I would not pursue partially overlapping submissions without editorial approval. Thank you for your attention.