Submission declined on 23 March 2026 by Dan arndt (talk). This draft is not adequately supported by reliable sources. Wikipedia's verifiability policy requires that all content be supported by reliable sources. Reliable sources include: reputable newspapers, magazines, academic journals, and books from respected publishers. Unacceptable sources include: personal blogs, social media, predatory publishers, most tabloids, and websites where anyone can contribute. Replace any unreliable sources with high-quality sources. If you cannot find a reliable source for the material, it should be removed. This draft reads like an essay or opinion piece. Wikipedia is not a place for original research or personal opinions. The draft should: summarize secondary sources: do not offer your own analysis or arguments; be written from a neutral point of view: represent the subject without bias, avoiding praise, criticism, or persuasive or promotional language; not contain original research: do not include new theories, unpublished ideas, or personal experiences. Instead, only summarize in your own words a range of independent, reliable, published sources that discuss the subject. If you would like to continue working on the submission, click on the "Edit" tab at the top of the window. If you have not resolved the issues listed above, your draft will be declined again and potentially deleted. If you need extra help, please ask us a question at the AfC Help Desk or get live help from experienced editors. Please do not remove reviewer comments or this notice until the submission is accepted. Where to get help If you need help editing or submitting your draft, please ask us a question at the AfC Help Desk or get live help from experienced editors. These venues are only for help with editing and the submission process, not to get reviews. If you need feedback on your draft, or if the review is taking a lot of time, you can try asking for help on the talk page of a relevant WikiProject. Some WikiProjects are more active than others so a speedy reply is not guaranteed. How to improve a draft Wikipedia:Contributing to Wikipedia – a basic overview on how to edit Wikipedia. Help:Wikitext – how to use the markup Help:Referencing for beginners – how to include references Wikipedia:Article development – how to develop your article Wikipedia:Writing better articles – how to improve your article Wikipedia:Verifiability – make sure your article includes reliable third-party sources You can also browse Wikipedia:Featured articles and Wikipedia:Good articles to find examples of Wikipedia's best writing on topics similar to your proposed article. Improving your odds of a speedy review To improve your odds of a faster review, tag your draft with relevant WikiProject tags using the button below. This will let reviewers know a new draft has been submitted in their area of interest. For instance, if you wrote about a female astronomer, you would want to add the Biography, Astronomy, and Women scientists tags. Add tags to your draft Editor resources Easy tools: Citation bot (help) | Advanced: Fix bare URLs Declined by Dan arndt 4 months ago. Last edited by Dan arndt 4 months ago. Reviewer: Inform author. Resubmit Please note that if the issues are not fixed, the draft will be declined again.

• Comment: All information provided needs to be backed with inline citations referencing verifiable secondary sources. Dan arndt (talk) 04:51, 23 March 2026 (UTC)

In mathematical logic and proof theory, the Prawitz embedding (also known as the Russell–Prawitz translation) is a method for embedding intuitionistic propositional logic into second-order intuitionistic logic.

The embedding demonstrates that all standard logical connectives (conjunction, disjunction, and the existential quantifier) can be defined using only implication and universal quantification over propositions.

The translation is named after Dag Prawitz, who detailed the embedding in his 1965 monograph Natural Deduction: A Proof-Theoretical Study. However, the core idea of defining logical constants in terms of higher-order quantification dates back to Bertrand Russell's 1903 work The Principles of Mathematics. It is often discussed in the context of System F in computer science, where it provides a way to encode algebraic data types.

The embedding maps formulas of intuitionistic propositional logic into the second-order fragment. Let ${\displaystyle X}$ be a propositional variable that does not occur free in ${\displaystyle A}$ or ${\displaystyle B}$. The standard definitions are as follows:

• Absurdity (Falsehood):

${\displaystyle \bot \equiv \forall X.X}$

• Conjunction:

${\displaystyle A\wedge B\equiv \forall X.(A\to B\to X)\to X}$

• Disjunction:

${\displaystyle A\vee B\equiv \forall X.(A\to X)\to (B\to X)\to X}$

In the context of second-order predicate logic, the existential quantifier can also be embedded:

• Existential Quantification:

${\displaystyle \exists x.A(x)\equiv \forall X.(\forall x.(A(x)\to X))\to X}$

The Prawitz embedding is significant because it shows that the "implication-universal" fragment of second-order logic is expressive enough to recover the full power of intuitionistic logic. In terms of the Curry–Howard correspondence, this corresponds to the fact that the polymorphic lambda calculus (System F) can represent data types like booleans, pairs, and sums without adding them as primitives.

• Natural deduction
• System F
• Proof-theoretic semantics
• Intuitionistic logic

• Prawitz, Dag (1965). Natural Deduction: A Proof-Theoretical Study. Almqvist & Wiksell.
• Russell, Bertrand (1903). The Principles of Mathematics. Cambridge University Press.