A Proposition Decomposition and Contradiction-Driven Reasoning System — Looking for Discussion and Collaborators

An independent researcher is proposing a reasoning system that decomposes propositions into sub-components and searches for contradictions through implication relations, rather than asking a large language model to directly judge whether two propositions conflict. The design separates probabilistic candidate generation from a formal logical verifier, with the stated hypothesis that actively pursuing collisions with existing propositions discovers contradictions more efficiently under limited generation and computational budgets. The proposal remains a research design rather than a completed system, and the author is seeking discussion, criticism, alternative approaches, and collaborators to implement or test it.

Abstract I am exploring a reasoning system that uses proposition decomposition and contradiction search rather than asking an LLM to directly judge whether two propositions are contradictory. The basic idea is to decompose propositions into smaller components, identify corresponding propositions through implication relations, and use these relations to search for contradictions. The system is intended to separate probabilistic exploration from a more reliable formal verification process. I am particularly interested in whether actively searching for contradictions can provide a useful direction for reasoning and exploration under a limited generation budget. This is still a research design rather than a completed system. I am looking for discussion, criticism, alternative approaches, and collaborators who may be interested in implementing or testing the idea. P → Q , meaning that if P holds, Q follows within the adopted formal system. The central system to be built is a contradiction checker . The basic I/O is deliberately simple. Input: Proposition P, Proposition Q Output: Whether P and Q contradict each other However, the two propositions are not compared directly as strings. The propositions are decomposed, and implication relations between propositions are used to identify parts that can be regarded as expressing the same subject or content; the resulting identification is then used to search for contradictions. Therefore, proposition identification is not merely a function for checking whether a decomposition is valid; it is itself a foundation of contradiction checking. The central hypothesis is that, compared with generating a large number of candidates without direction, a search that actively pursues collisions with existing propositions may discover contradictions more efficiently under limited generation and computational budgets. This is a hypothesis to be supported or refuted experimentally. Proposition P Proposition Q ↓ ↓ Proposition decomposition / normalization ↓ ↓ Acquisition of implication / compositional relations ↓ ↓ Proposition identification / correspondence ↓ Collision search ↓ Formal logical verification ↓ CONTRADICTION / CONSISTENT / UNKNOWN If a learning system is connected later, a search loop is added here. Collision candidate generation ↓ Verifier ↓ Reward ↓ Next candidate generation The checker itself and the search process that looks for candidates are kept separate. Here, identification does not mean exact string matching. A proposition is decomposed into constituent sub-propositions, and the implication relations between them and existing propositions are examined. Conceptually, for example, P → A → B → C Q → A → B → C means that P and Q share at least the common logical structure A, B, and C. Likewise, P → A Q → B B → A means that, although P and Q are superficially different, they become comparable with respect to A. Therefore, identification and correspondence use: Truth value and the content/structure of a proposition are treated separately. For example, p and ¬p should be treated as corresponding positive and negative forms of the same underlying proposition, rather than as completely unrelated propositions. Proposition identification has at least two uses. When an original proposition P is decomposed into P1, P2, ..., Pn the system checks whether the content reconstructed from the decomposed elements has the same meaning, or the same specified implication relations, as P. For a simple AND decomposition, for example, P ↔ P1 ∧ P2 ∧ ... ∧ Pn can be verified. When comparing P and Q, the propositions derived from both are first put into correspondence. Then, if a relation such as P → A Q → ¬A is found for the same subject/content, this becomes a candidate for testing whether P and Q can hold simultaneously. Longer paths are also allowed. P → A → B → C Q → D → ¬C D → C In this case, P and Q respectively imply C and ¬C, so they form a collision candidate. Therefore, proposition identification/correspondence is not merely a preprocessing step for contradiction checking; it constructs the comparison space in which contradictions can be discovered. The initial version primarily targets propositional logic. Input: P Q Output: CONTRADICTION CONSISTENT UNKNOWN Definitions: “Failure to find a contradiction” is not treated as “consistent.” Within domains such as propositional logic where finite search is possible, the system should be deterministic whenever possible. P and Q are not compared in a single step. Both are decomposed, and propositions that can be derived from them are expanded step by step. Conceptually, paths such as P → A → B → C Q → D → E → ¬C are constructed, and the system checks whether positive and negative forms eventually appear for content that can be identified as the same. The ideal form is to explore combinations of propositions derived from P and Q as broadly as possible and discover collisions such as A and ¬A B and ¬B C and ¬C ... However, enumerating all consequences leads to combinatorial explosion, so the search process selects promising directions. Candidate generation is not treated as undirected random search. For example, given an existing proposition P, the search objective is: Generate a proposition that may collide with P. However, the system must consider the possibility that a search may degenerate into simply generating ¬P repeatedly. The appropriate reward structure is itself an experimental variable. Initial reward candidates: Collision found → positive reward No collision found → low / 0 reward Could not be formalized → low / negative reward As needed, additional terms such as the number of inference steps to the collision, decomposition validity, and redundancy may be added. A “non-trivial collision” is not required as a formal definition. The central comparison is: Undirected search vs. Collision-seeking search with the collision discovery efficiency compared under the same generation and computational budgets. Decomposition is not simply “the more fine-grained, the better.” At minimum, the following properties are required. Logical content should be preserved between the original and decomposed forms. Original proposition ↓ decomposition P1, P2, ..., Pn ↓ reconstruction Equivalent to the original proposition / satisfies the specified implication relations The system checks whether each component is actually necessary. If removing an element Pi still allows the original proposition to be fully preserved from the remaining elements, Pi may be treated as a redundant component. Conceptually, one can verify conditions such as: P1 ∧ ... ∧ Pn entails P P1 ∧ ... ∧ ¬Pi ∧ ... ∧ Pn does not entail P A component is not rewarded merely for making the representation finer. The current specification does not claim that this problem is necessarily NP-hard. The intended claim is only that searching for minimal sufficient decompositions or minimal evidence sets may cause combinatorial explosion. Propositions are not treated as mere strings, but as nodes connected by relations. Example: P → A A → B B → C Q → D D → C This shows that P and Q both imply C. With negation included, P → A → B → C Q → D → ¬C can produce a collision candidate. The proposition graph is not the final truth checker. Its main roles are to: Final logical checking is performed by a separate formal verifier. Not every proposition needs to be compared with every other proposition. First, implication relations, structure, and correspondence of subjects are used to narrow the set to propositions that may be describing the same thing. After candidate correspondences are produced, an LLM may be used for semantic comparison of atomic propositions that cannot be formally matched. Do not insist on complete mechanical determination here. The LLM is used as an auxiliary mechanism for constructing comparison targets, not as the final contradiction checker . Unknown propositions are not forcibly assigned a truth value. Decidable within the formal system → formal verification Not decidable within the formal system → UNKNOWN Search and experiments for acquiring external information are future extensions and are not the center of the minimal implementation. After the checker is completed, an LLM may be connected as a search process. LLM ↓ Generate proposition decompositions / derived propositions / collision candidates ↓ Formal verifier ↓ Reward ↓ Next candidate generation Multiple candidates are generated and evaluated through the verifier. At this stage, reinforcement learning such as GRPO may be used. In production, LoRA / QLoRA may be applied to an existing LLM, and Unsloth or similar tools may be used as the training infrastructure. The training infrastructure itself is not the research target. The first experiment is not intended to determine whether an “intelligent AI” can be built. It tests the following single point: Under the same generation budget, can collision-seeking search discover more contradictions than undirected search? The comparison should be controlled for quantities such as: Number of generated candidates Token count Computation time Candidate evaluation measures include: Number of discovered contradictions / number of generated candidates Number of discovered contradictions / token count Number of discovered contradictions / computation time A toy dataset may be used initially, but the production code and toy-specific code should not be designed as separate systems . The same design should allow the model size to be changed while preserving the system being evaluated. In principle, the LLM is not used to make the final judgment “Do these two propositions contradict?” This is the most important point. Do not treat a formally proven equivalence and an LLM judgment that two statements are similar as the same kind of result. Mutual information represents statistical dependence over probability distributions. Implication represents a relation within a logical system. The present method is not proposed as a direct alternative definition of mutual information. It is positioned as a method for making comparable information explicit as logical structure. Do not claim that every natural-language proposition can be determined with certainty. First specify the formal system being targeted, and then seek as much rigor and completeness as possible within that scope. Conserve data and reduce hypotheses with small experiments before spending large amounts of computation. Use intuition to generate hypotheses, but use explicit definitions, predictions, and falsification conditions during verification. The following supplementary note describes the broader motivation that led me to focus on trial-and-error search and the direction of reasoning. The history of academic discoveries has, in most cases, been driven by trial and error. If there were a universal algorithm capable of solving every unsolved problem, one would expect it to have been discovered during the last 2,000 years. It has not. For details, please search for the P vs NP problem. Since there is no universal algorithm for problem solving, the only way to approach unsolved problems may be to “search through them the hard way.” Therefore, is it really correct to try to solve unsolved problems with an algorithm called an LLM? Even if trial and error can be performed inside a model, I suspect it would remain very limited. There is research suggesting that OpenAI’s o1, particularly the o3 series, can exhibit trial-and-error behavior, and I think this is directionally correct. However, many problems remain: Personally, I think the last two are especially important. I have tried to tackle them, but they are quite difficult. Whenever I think about the problems of AI, extrapolation seems to appear as an issue everywhere. But perhaps humans also extrapolate by performing an enormous amount of search.