Q0 (mathematical logic)
Q0 என்பது பீட்டர் ஆண்ட்ரூஸின் எளிமையாக தட்டச்சு செய்யப்பட்ட லாம்ப்டா கால்குலஸின் சூத்திரமாகும், மேலும் இது முதல்-வரிசை தர்க்கம் மற்றும் தொகுப்புக் கோட்பாட்டுடன் ஒப்பிடக்கூடிய கணிதத்திற்கான அடித்தளத்தை வழங்குகிறது. இது உயர்-வரிசை தர்க்கத்தின் ஒரு வடிவமாகும் மற்றும் HOL தேற்றத்தின் பழமொழி குடும்பத்தின் தர்க்கங்களுடன் நெருக்கமாக தொடர்புடையது. TPS மற்றும் ETPS அமைப்புகளை நிரூபிக்கும் தேற்றம் Q0 ஐ அடிப்படையாகக் கொண்டது. ஆகஸ்ட் 2009 இல், உயர்-வரிசை தேற்றத்தை நிரூபிக்கும் அமைப்புகளுக்கு இடையிலான முதல் போட்டியை டி. பி. எஸ் வென்றது. Q0 இன் கோட்பாடுகள் இந்த அமைப்பில் ஐந்து கோட்பாடுகள் மட்டுமே உள்ளன, அவை பின்வருமாறு கூறப்படலாம்ஃ (கோட்பாடுகள் 2,3 மற்றும் 4 ஆகியவை கோட்பாடுகளின் திட்டங்களாகும்-ஒத்த கோட்பாடுகளின் குடும்பங்கள். மூலக்கூறு 2 மற்றும் மூலக்கூறு 3 இன் நிகழ்வுகள் மாறிகள் மற்றும் மாறிலிகளின் வகைகளால் மட்டுமே வேறுபடுகின்றன, ஆனால் மூலக்கூறு 4 இன் நிகழ்வுகள் A மற்றும் B க்கு பதிலாக எந்த வெளிப்பாட்டையும் கொண்டிருக்கலாம்.) சந்தா "ஓ" என்பது பூலியன் மதிப்புகளுக்கான வகை சின்னமாகும், மேலும் சந்தா "ஐ" என்பது தனிப்பட்ட (பூலியன் அல்லாத) மதிப்புகளுக்கான வகை சின்னமாகும். இவற்றின் வரிசைகள் செயல்பாடுகளின் வகைகளைக் குறிக்கின்றன, மேலும் வெவ்வேறு செயல்பாட்டு வகைகளை வேறுபடுத்துவதற்காக அடைப்புக்குறிகளைச் சேர்க்கலாம். α மற்றும் β போன்ற கிரேக்க எழுத்துக்கள் வகை குறியீடுகளுக்கான சொற்பொருள் மாறிகள் ஆகும். போல்ட் கேபிடல் எழுத்துக்கள், மற்றும் WFF களுக்கான சொற்பொருள் மாறிகள், மற்றும் போல்ட் லோயர் கேஸ் எழுத்துக்கள் போன்றவை மாறிகளுக்கான சொற்பொருள் மாறிகள் ஆகும். அனைத்து இலவச நிகழ்வுகளிலும் சொற்பொருள் மாற்றீட்டைக் குறிக்கிறது. ஒரே பழமையான மாறிலிகள், ஒவ்வொரு வகை α இன் உறுப்பினர்களின் சமத்துவத்தைக் குறிக்கின்றன, மேலும், தனிநபர்களுக்கான விளக்க ஆபரேட்டரைக் குறிக்கின்றன, சரியாக ஒரு தனிநபரைக் கொண்ட ஒரு தொகுப்பின் தனித்துவமான உறுப்பு. குறியீடுகள் λ மற்றும் அடைப்புக்குறிகள் ("[" மற்றும் "]") மொழியின் தொடரியல் ஆகும். மற்ற அனைத்து குறியீடுகளும் இவற்றைக் கொண்ட சொற்களுக்கான சுருக்கங்களாகும், இதில் அளவீடுகள் மற்றும் HE அடங்கும். கோட்பாடு 4 இல், உள்ளதற்கு இலவசமாக இருக்க வேண்டும், அதாவது மாற்றீடு என்பது மாற்றீட்டின் விளைவாக பிணைக்கப்படுவதற்கான இலவச மாறிகளின் எந்தவொரு நிகழ்வுகளையும் ஏற்படுத்தாது. கோட்பாடுகள் பற்றி கோட்பாடு 1 மட்டுமே பூலியன் மதிப்புகள் என்ற கருத்தை வெளிப்படுத்துகிறது. ஆக்சியம் ஸ்கீமாக்கள் 2α மற்றும் 3αβ ஆகியவை செயல்பாடுகளின் அடிப்படை பண்புகளை வெளிப்படுத்துகின்றன. ஆக்சியம் ஸ்கீமா 4 λ குறியீட்டின் தன்மையை வரையறுக்கிறது. தேர்வு ஆபரேட்டர் என்பது தனிநபர்களின் சமத்துவ செயல்பாட்டின் தலைகீழ் என்று கோட்பாடு 5 கூறுகிறது. (ஒரு வாதத்தைப் பொறுத்தவரை, அந்த தனிநபரை தனிநபரைக் கொண்ட தொகுப்பு/முன்கணிப்புக்கு வரைபடமாக்குகிறது. Q0 இல், ஒரு சுருக்கமாகும், இது ஒரு சுருக்கமாகும்). இந்த ஆபரேட்டர் திட்டவட்டமான விளக்க ஆபரேட்டர் என்றும் அழைக்கப்படுகிறார். இதில், மாற்று செயல்முறையை உடைக்கும் ஐந்து துணைப் பகுதிகளாக ஆக்சியம் 4 உருவாக்கப்பட்டது. இங்கே கொடுக்கப்பட்டுள்ள கோட்பாடு ஒரு மாற்றாக விவாதிக்கப்பட்டு துணைப் பகுதிகளிலிருந்து நிரூபிக்கப்பட்டுள்ளது. தர்க்கரீதியான மையத்தின் விரிவாக்கங்கள் ஆண்ட்ரூஸ் இந்த தர்க்கத்தை அனைத்து வகையான தொகுப்புகளுக்கான தேர்வு ஆபரேட்டர்களின் வரையறைகளுடன் விரிவுபடுத்துகிறது, இதனால் ஒரு தேற்றம் (எண் 5309). வேறு வார்த்தைகளில் கூறுவதானால், அனைத்து வகைகளும் ஒரு திட்டவட்டமான விளக்க ஆபரேட்டரைக் கொண்டுள்ளன. இது ஒரு பழமைவாத நீட்டிப்பாகும், எனவே மையப்பகுதி சீராக இருந்தால் நீட்டிக்கப்பட்ட அமைப்பு சீராக இருக்கும். அவர் ஒரு கூடுதல் கோட்பாடு 6 ஐ முன்வைக்கிறார், இது முடிவிலியின் சமமான மாற்று கோட்பாடுகளுடன், எண்ணற்ற பல தனிநபர்கள் இருப்பதாகக் கூறுகிறது. வகைக் கோட்பாட்டை அடிப்படையாகக் கொண்ட வகைக் கோட்பாடு மற்றும் ஆதார உதவியாளர்களின் பல சூத்திரங்களைப் போலல்லாமல், ஓ மற்றும் ஐ தவிர வேறு அடிப்படை வகைகளுக்கு க்யூ0 வழங்கவில்லை, எனவே எடுத்துக்காட்டாக வரையறுக்கப்பட்ட கார்டினல் எண்கள் எளிய வகைக் கோட்பாட்டின் அர்த்தத்தில் ஒரு வகையைக் காட்டிலும் வழக்கமான பீனோ அனுமானங்களுக்குக் கீழ்ப்படும் தனிநபர்களின் தொகுப்புகளாக கட்டமைக்கப்படுகின்றன. Q0 Q0 இல் உள்ள அனுமானம் அனுமானத்தின் ஒற்றை விதியைக் கொண்டுள்ளது. விதி ஆர். இன் இன் நிகழ்வு உடனடியாக முன் (ஒரு மாறியின் நிகழ்வு) இல்லை என்றால், இன் இன் ஒரு நிகழ்வை மாற்றுவதன் விளைவாக இருந்து மற்றும் ஊகிக்க. அனுமானம் R′ இன் பெறப்பட்ட விதி H. விதி R′ கருதுகோள்களின் தொகுப்பிலிருந்து பகுத்தறிவுக்கு உதவுகிறது. ஒரு நிகழ்வை ஒரு நிகழ்வால் மாற்றுவதன் மூலம், மற்றும், மற்றும் பெறப்பட்டால், பின்வருமாறு வழங்கப்படும்ஃ இன் நிகழ்வு என்பது உடனடியாக முந்தைய ஒரு மாறியின் நிகழ்வு அல்ல, மேலும் எந்த மாறியும் ஃப்ரீ இன் மற்றும் ஒரு உறுப்பினரும் பிணைக்கப்படவில்லை. குறிப்புஃ இன் மூலம் மாற்றுவதற்கான கட்டுப்பாடு ஒரு கருதுகோள் இரண்டிலும் எந்தவொரு மாறியும் இலவசம் மற்றும் மாற்றப்பட்ட பிறகு இரண்டிலும் ஒரே மதிப்பைக் கொண்டிருக்க தொடர்ந்து கட்டுப்படுத்தப்படுவதை உறுதி செய்கிறது. Q0 க்கான கழித்தல் தேற்றம், விதி R′ ஐப் பயன்படுத்தும் கருதுகோள்களின் சான்றுகளை கருதுகோள்கள் இல்லாமல் ஆதாரங்களாக மாற்றலாம் மற்றும் விதி R ஐப் பயன்படுத்தலாம் என்பதைக் காட்டுகிறது. சில ஒத்த அமைப்புகளைப் போலல்லாமல், Q0 இல் உள்ள அனுமானம் ஒரு WFF க்குள் எந்த ஆழத்திலும் ஒரு துணை வெளிப்பாட்டை சமமான வெளிப்பாட்டுடன் மாற்றுகிறது. எனவே உதாரணமாக கொடுக்கப்பட்ட கோட்பாடுகள்ஃ 1. 2. மற்றும் உண்மை என்னவென்றால், அளவீட்டை அகற்றாமல் நாம் தொடரலாம்ஃ 3. ஏ மற்றும் பி 4 க்கு உடனடி. விதி ஆர் வரி 3 ஐப் பயன்படுத்தி வரி 1 ஆக மாற்றப்படுகிறது. குறிப்புகள் குறிப்புகள் மேலும் படிக்க மேலும் ஆழமாக Q0 பற்றிய ஒரு விளக்கம்; ஸ்டான்போர்ட் என்சைக்ளோபீடியா ஆஃப் தத்துவத்தில் சர்ச்சின் வகை கோட்பாடு குறித்த கட்டுரையின் ஒரு பகுதி. கணித தர்க்கவியல் பற்றிய ஒரு கண்ணோட்டம் (Q0 இன் பல்வேறு வாரிசுகள் உட்பட): கணிதத்தின் அடித்தளங்கள். மரபியல் மற்றும் கண்ணோட்டம்ஃ 10.4444/100.111. கணினி அறிவியலில் தர்க்கம்