Contents

foundations

# Contents

## Idea

A higher-order logic is any logic which features higher-order predicates, which are predicates of predicates or of operations. If we think of a predicate as a function to truth values, then a higher-order predicate is a function on a power set or a function set.

Typed higher-order logic may be called higher-order type theory. Typed higher-order intuitionistic logic is often identified with the internal logic of a topos.

Higher-order logic in general could be thought of as a first order theory with dependent types. There is a type $V$ called the domain of discourse, and for each type $T$ and each term $t:T$, a type of predicates on $T$ $\mathcal{P}(T)$ whose terms $P(t):\mathcal{P}(T)(t)$ are propositions dependent on $t$. The system $(\mathcal{U}, V:\mathcal{U}, \mathcal{P}:\mathcal{U}\rightarrow\mathcal{U})$ consisting of the type universe $\mathcal{U}$, the domain of discourse $V$, and the power type functor $\mathcal{P}$ is a natural numbers object.

Last revised on March 3, 2021 at 12:42:53. See the history of this page for a list of all contributions to it.
{"ft_lang_label":"__label__en","ft_lang_prob":0.91921014,"math_prob":0.99590075,"size":1029,"snap":"2021-04-2021-17","text_gpt3_token_len":217,"char_repetition_ratio":0.17365853,"word_repetition_ratio":0.0,"special_character_ratio":0.20991254,"punctuation_ratio":0.0959596,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9988166,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2021-04-23T17:51:59Z\",\"WARC-Record-ID\":\"<urn:uuid:4185413d-a5b2-4c16-8c27-b61f50c3e626>\",\"Content-Length\":\"25902\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:d8e9cf69-faa0-486b-8100-fe85c456f66b>\",\"WARC-Concurrent-To\":\"<urn:uuid:056a45be-aaec-4b92-b7cf-7922d1242185>\",\"WARC-IP-Address\":\"104.21.81.15\",\"WARC-Target-URI\":\"https://ncatlab.org/nlab/show/higher-order+logic\",\"WARC-Payload-Digest\":\"sha1:CB2EWGTP4PBVAG6NBXPX5PCH7TWWCUFB\",\"WARC-Block-Digest\":\"sha1:HS6ULQVHUPXZHQVCTG6EOO77LYOZJDHL\",\"WARC-Identified-Payload-Type\":\"application/xhtml+xml\",\"warc_filename\":\"/cc_download/warc_2021/CC-MAIN-2021-17/CC-MAIN-2021-17_segments_1618039596883.98_warc_CC-MAIN-20210423161713-20210423191713-00393.warc.gz\"}"}